refactor(LinearAlgebra/BilinForm): Remove structure BilinForm from …

…Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` (#11278)

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

Closes: #10553 

This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm` and `LinearAlgebra/SesquilinearForm` but that can be sorted out in subsequent PRs.

Supersedes: 

- #11057
- #11032
- #10432
- #10422



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Vierkantor <[email protected]>

Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

@@ -17,9 +17,13 @@ import Mathlib.LinearAlgebra.BilinearForm.Properties
 Properly develop the material in the context of lattices.
 -/
 
+open LinearMap (BilinForm)
+
 variable {R S M} [CommRing R] [Field S] [AddCommGroup M]
 variable [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M]
 
+namespace LinearMap
+
 namespace BilinForm
 
 variable (B : BilinForm S M)
@@ -31,7 +35,8 @@ def dualSubmodule (N : Submodule R M) : Submodule R M where
   zero_mem' y _ := by rw [B.zero_left]; exact zero_mem _
   smul_mem' r a ha y hy := by
     convert (1 : Submodule R S).smul_mem r (ha y hy)
-    rw [← IsScalarTower.algebraMap_smul S r a, bilin_smul_left, Algebra.smul_def]
+    rw [← IsScalarTower.algebraMap_smul S r a]
+    simp only [algebraMap_smul, map_smul_of_tower, LinearMap.smul_apply]
 
 lemma mem_dualSubmodule {N : Submodule R M} {x} :
     x ∈ B.dualSubmodule N ↔ ∀ y ∈ N, B x y ∈ (1 : Submodule R S) := Iff.rfl
@@ -96,11 +101,12 @@ lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι]
   · rw [Submodule.span_le]
     rintro _ ⟨i, rfl⟩ y hy
     obtain ⟨f, rfl⟩ := (mem_span_range_iff_exists_fun _).mp hy
-    simp only [sum_right, bilin_smul_right]
+    simp only [map_sum, map_smul]
     apply sum_mem
     rintro j -
-    rw [← IsScalarTower.algebraMap_smul S (f j), B.bilin_smul_right, apply_dualBasis_left,
-      mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
+    rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]
+    simp_rw [apply_dualBasis_left]
+    rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
     exact ⟨_, rfl⟩
 
 lemma dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι]