feat: port FieldTheory.SplittingField.Construction (#4891)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · Jun 25, 2023 · cf02c71 · cf02c71
1 parent e3c0770
commit cf02c71
Show file tree

Hide file tree

Showing 3 changed files with 421 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1745,6 +1745,7 @@ import Mathlib.FieldTheory.PerfectClosure
 import Mathlib.FieldTheory.RatFunc
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SeparableDegree
+import Mathlib.FieldTheory.SplittingField.Construction
 import Mathlib.FieldTheory.SplittingField.IsSplittingField
 import Mathlib.FieldTheory.Subfield
 import Mathlib.FieldTheory.Tower

diff --git a/Mathlib/Data/MvPolynomial/Basic.lean b/Mathlib/Data/MvPolynomial/Basic.lean
@@ -150,6 +150,14 @@ instance isScalarTower' [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] :
   IsScalarTower.right
 #align mv_polynomial.is_scalar_tower' MvPolynomial.isScalarTower'
 
+--Porting note: new instance
+instance isScalarTower_right [CommSemiring R] [CommSemiring S₁] [DistribSMul R S₁]
+    [IsScalarTower R S₁ S₁] : IsScalarTower R (MvPolynomial σ S₁) (MvPolynomial σ S₁) :=
+  ⟨by
+    rintro x p q
+    dsimp [MvPolynomial] at p q ⊢
+    rw [smul_mul_assoc]⟩
+
 /-- If `R` is a subsingleton, then `MvPolynomial σ R` has a unique element -/
 instance unique [CommSemiring R] [Subsingleton R] : Unique (MvPolynomial σ R) :=
   AddMonoidAlgebra.unique