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>

Author: 4 people

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

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