chore(LinearAlgebra/QuadraticForm): scalar tower instances and cleanup (#6433)

This is needed to state that the base change of a quadratic form is itself a linear operation.

Also adds a linear version of `BilinForm.toQuadraticForm`, and cleans up some docstrings that had been mangled by `fix-comments.py`

Author: eric-wieser

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -68,7 +68,7 @@ quadratic form, homogeneous polynomial, quadratic polynomial
 
 universe u v w
 
-variable {S : Type _}
+variable {S T : Type _}
 
 variable {R R₁ : Type _} {M : Type _}
 
@@ -365,7 +365,8 @@ variable [Semiring R] [AddCommMonoid M] [Module R M]
 
 section SMul
 
-variable [Monoid S] [DistribMulAction S R] [SMulCommClass S R R]
+variable [Monoid S] [Monoid T] [DistribMulAction S R] [DistribMulAction T R]
+variable [SMulCommClass S R R] [SMulCommClass T R R]
 
 /-- `QuadraticForm R M` inherits the scalar action from any algebra over `R`.
 
@@ -388,6 +389,12 @@ theorem smul_apply (a : S) (Q : QuadraticForm R M) (x : M) : (a • Q) x = a •
   rfl
 #align quadratic_form.smul_apply QuadraticForm.smul_apply
 
+instance [SMulCommClass S T R] : SMulCommClass S T (QuadraticForm R M) where
+  smul_comm _s _t _q := ext <| fun _ => smul_comm _ _ _
+
+instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticForm R M) where
+  smul_assoc _s _t _q := ext <| fun _ => smul_assoc _ _ _
+
 end SMul
 
 instance : Zero (QuadraticForm R M) :=
@@ -675,7 +682,7 @@ theorem toQuadraticForm_smul [Monoid S] [DistribMulAction S R] [SMulCommClass S
 
 section
 
-variable (R M)
+variable (S R M)
 
 /-- `BilinForm.toQuadraticForm` as an additive homomorphism -/
 @[simps]
@@ -685,6 +692,14 @@ def toQuadraticFormAddMonoidHom : BilinForm R M →+ QuadraticForm R M where
   map_add' := toQuadraticForm_add
 #align bilin_form.to_quadratic_form_add_monoid_hom BilinForm.toQuadraticFormAddMonoidHom
 
+/-- `BilinForm.toQuadraticForm` as a linear map -/
+@[simps!]
+def toQuadraticFormLinearMap [Semiring S] [Module S R] [SMulCommClass S R R] :
+    BilinForm R M →ₗ[S] QuadraticForm R M where
+  toFun := toQuadraticForm
+  map_smul' := toQuadraticForm_smul
+  map_add' := toQuadraticForm_add
+
 end
 
 @[simp]
@@ -754,9 +769,9 @@ variable [Invertible (2 : R)] {B₁ : BilinForm R M}
 associated symmetric bilinear form.  As provided here, this has the structure of an `S`-linear map
 where `S` is a commutative subring of `R`.
 
-Over a commutative ring, use `Associated`, which gives an `R`-linear map.  Over a general ring with
-no nontrivial distinguished commutative subring, use `Associated'`, which gives an additive
-homomorphism (or more precisely a `ℤ`-linear map.) -/
+Over a commutative ring, use `QuadraticForm.associated`, which gives an `R`-linear map.  Over a
+general ring with no nontrivial distinguished commutative subring, use `QuadraticForm.associated'`,
+which gives an additive homomorphism (or more precisely a `ℤ`-linear map.) -/
 def associatedHom : QuadraticForm R M →ₗ[S] BilinForm R M where
   toFun Q :=
     ((· • ·) : Submonoid.center R → BilinForm R M → BilinForm R M)
@@ -850,7 +865,7 @@ variable [CommRing R₁] [AddCommGroup M] [Module R₁ M]
 variable [Invertible (2 : R₁)]
 
 -- Note:  When possible, rather than writing lemmas about `associated`, write a lemma applying to
--- the more general `AssociatedHom` and place it in the previous section.
+-- the more general `associatedHom` and place it in the previous section.
 /-- `associated` is the linear map that sends a quadratic form over a commutative ring to its
 associated symmetric bilinear form. -/
 abbrev associated : QuadraticForm R₁ M →ₗ[R₁] BilinForm R₁ M :=