chore(LinearAlgebra): Introduce a LinearMap.BilinForm alias (#10632)

This is one of the steps in #10553.

Once we eliminate `_root_.BilinForm`, we can drop the `LinearMap.` prefix.

Requested on Zulip [by me](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962) (2021), [by @kmill](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60/near/310675731) (2022), and perhaps one or two other places.



Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>

Mathlib/Algebra/Lie/Killing.lean

@@ -64,7 +64,7 @@ namespace LieModule
 
 /-- A finite, free representation of a Lie algebra `L` induces a bilinear form on `L` called
 the trace Form. See also `killingForm`. -/
-noncomputable def traceForm : L →ₗ[R] L →ₗ[R] R :=
+noncomputable def traceForm : LinearMap.BilinForm R L :=
   ((LinearMap.mul _ _).compl₁₂ (φ).toLinearMap (φ).toLinearMap).compr₂ (trace R M)
 
 lemma traceForm_apply_apply (x y : L) :
@@ -183,7 +183,7 @@ lemma traceForm_apply_eq_zero_of_mem_lcs_of_mem_center {x y : L}
 invariant (in the sense that the action of `L` is skew-adjoint wrt `B`) then components of the
 Fitting decomposition of `M` are orthogonal wrt `B`. -/
 lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
-    {B : M →ₗ[R] M →ₗ[R] R} (hB : ∀ (x : L) (m n : M), B ⁅x, m⁆ n = - B m ⁅x, n⁆)
+    {B : LinearMap.BilinForm R M} (hB : ∀ (x : L) (m n : M), B ⁅x, m⁆ n = - B m ⁅x, n⁆)
     {m₀ m₁ : M} (hm₀ : m₀ ∈ weightSpace M (0 : L → R)) (hm₁ : m₁ ∈ posFittingComp R L M) :
     B m₀ m₁ = 0 := by
   replace hB : ∀ x (k : ℕ) m n, B m ((φ x ^ k) n) = (- 1 : R) ^ k • B ((φ x ^ k) m) n := by
@@ -341,7 +341,7 @@ variable [Module.Free R L] [Module.Finite R L]
 /-- A finite, free (as an `R`-module) Lie algebra `L` carries a bilinear form on `L`.
 
 This is a specialisation of `LieModule.traceForm` to the adjoint representation of `L`. -/
-noncomputable abbrev killingForm : L →ₗ[R] L →ₗ[R] R := LieModule.traceForm R L L
+noncomputable abbrev killingForm : LinearMap.BilinForm R L := LieModule.traceForm R L L
 
 lemma killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting
     (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H]

Mathlib/Algebra/Module/Submodule/Bilinear.lean

@@ -176,7 +176,7 @@ end Submodule
 lemma LinearMap.ker_restrictBilinear_eq_of_codisjoint
     {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
     {p q : Submodule R M} (hpq : Codisjoint p q)
-    {B : M →ₗ[R] M →ₗ[R] R} (hB : ∀ x ∈ p, ∀ y ∈ q, B x y = 0) :
+    {B : LinearMap.BilinForm R M} (hB : ∀ x ∈ p, ∀ y ∈ q, B x y = 0) :
     LinearMap.ker (p.restrictBilinear B) = (LinearMap.ker B).comap p.subtype := by
   ext ⟨z, hz⟩
   simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coeSubtype]

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -399,9 +399,15 @@ variable {R M}
 theorem lsmul_apply (r : R) (m : M) : lsmul R M r m = r • m := rfl
 #align linear_map.lsmul_apply LinearMap.lsmul_apply
 
+variable (R M) in
+/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`.
+
+This should eventually replace `_root_.BilinForm`. -/
+protected abbrev BilinForm : Type _ := M →ₗ[R] M →ₗ[R] R
+
 /-- The restriction of a bilinear form to a submodule. -/
-abbrev _root_.Submodule.restrictBilinear (p : Submodule R M) (f : M →ₗ[R] M →ₗ[R] R) :
-    p →ₗ[R] p →ₗ[R] R :=
+abbrev _root_.Submodule.restrictBilinear (p : Submodule R M) (f : LinearMap.BilinForm R M) :
+    LinearMap.BilinForm R p :=
   f.compl₁₂ p.subtype p.subtype
 
 end CommSemiring

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -142,7 +142,8 @@ structure QuadraticForm (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoi
     where
   toFun : M → R
   toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = a * a * toFun x
-  exists_companion' : ∃ B : M →ₗ[R] M →ₗ[R] R, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y
+  exists_companion' :
+    ∃ B : LinearMap.BilinForm R M, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y
 #align quadratic_form QuadraticForm
 
 namespace QuadraticForm
@@ -218,7 +219,7 @@ theorem map_smul (a : R) (x : M) : Q (a • x) = a * a * Q x :=
   Q.toFun_smul a x
 #align quadratic_form.map_smul QuadraticForm.map_smul
 
-theorem exists_companion : ∃ B : M →ₗ[R] M →ₗ[R] R, ∀ x y, Q (x + y) = Q x + Q y + B x y :=
+theorem exists_companion : ∃ B : LinearMap.BilinForm R M, ∀ x y, Q (x + y) = Q x + Q y + B x y :=
   Q.exists_companion'
 #align quadratic_form.exists_companion QuadraticForm.exists_companion
 
@@ -334,7 +335,7 @@ def polarBilin : BilinForm R M where
 
 /-- `QuadraticForm.polar` as a bilinear map -/
 @[simps!]
-def polarLinearMap₂ : M →ₗ[R] M →ₗ[R] R :=
+def polarLinearMap₂ : LinearMap.BilinForm R M :=
   LinearMap.mk₂ R (polar Q) (polar_add_left Q) (polar_smul_left Q) (polar_add_right Q)
   (polar_smul_right Q)
 
@@ -664,7 +665,7 @@ section Semiring
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
 /-- A bilinear map into `R` gives a quadratic form by applying the argument twice. -/
-def _root_.LinearMap.toQuadraticForm (B : M →ₗ[R] M →ₗ[R] R) : QuadraticForm R M where
+def _root_.LinearMap.toQuadraticForm (B : LinearMap.BilinForm R M) : QuadraticForm R M where
   toFun x := B x x
   toFun_smul a x := by
     simp only [SMulHomClass.map_smul, LinearMap.smul_apply, smul_eq_mul, mul_assoc]

Mathlib/LinearAlgebra/SesquilinearForm.lean

@@ -242,7 +242,7 @@ theorem domRestrict (H : B.IsSymm) (p : Submodule R M) : (B.domRestrict₁₂ p
 
 end IsSymm
 
-theorem isSymm_iff_eq_flip {B : M →ₗ[R] M →ₗ[R] R} : B.IsSymm ↔ B = B.flip := by
+theorem isSymm_iff_eq_flip {B : LinearMap.BilinForm R M} : B.IsSymm ↔ B = B.flip := by
   constructor <;> intro h
   · ext
     rw [← h, flip_apply, RingHom.id_apply]