refactor(LinearAlgebra/BilinearForm/Properties): Restrict the definition of BilinForm.IsSymm to commutative semiring

Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

@@ -64,15 +64,15 @@ theorem ne_zero_of_not_isOrtho_self {B : BilinForm K V} (x : V) (hx₁ : ¬B.IsO
   fun hx₂ => hx₁ (hx₂.symm ▸ isOrtho_zero_left _)
 #align bilin_form.ne_zero_of_not_is_ortho_self BilinForm.ne_zero_of_not_isOrtho_self
 
-theorem IsRefl.ortho_comm (H : B.IsRefl) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x :=
+theorem IsRefl.ortho_comm (H : B₂.IsRefl) {x y : M₂} : IsOrtho B₂ x y ↔ IsOrtho B₂ y x :=
   ⟨eq_zero H, eq_zero H⟩
 #align bilin_form.is_refl.ortho_comm BilinForm.IsRefl.ortho_comm
 
-theorem IsAlt.ortho_comm (H : B₁.IsAlt) {x y : M₁} : IsOrtho B₁ x y ↔ IsOrtho B₁ y x :=
+theorem IsAlt.ortho_comm (H : B₃.IsAlt) {x y : M₃} : IsOrtho B₃ x y ↔ IsOrtho B₃ y x :=
   H.isRefl.ortho_comm
 #align bilin_form.is_alt.ortho_comm BilinForm.IsAlt.ortho_comm
 
-theorem IsSymm.ortho_comm (H : B.IsSymm) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x :=
+theorem IsSymm.ortho_comm (H : B₂.IsSymm) {x y : M₂} : IsOrtho B₂ x y ↔ IsOrtho B₂ y x :=
   H.isRefl.ortho_comm
 #align bilin_form.is_symm.ortho_comm BilinForm.IsSymm.ortho_comm
 
@@ -150,7 +150,7 @@ def orthogonal (B : BilinForm R M) (N : Submodule R M) : Submodule R M where
     rw [IsOrtho, smul_right, show B n x = 0 from hx n hn, mul_zero]
 #align bilin_form.orthogonal BilinForm.orthogonal
 
-variable {N L : Submodule R M}
+variable {N L : Submodule R M} {N₂ : Submodule R₂ M₂}
 
 @[simp]
 theorem mem_orthogonal_iff {N : Submodule R M} {m : M} :
@@ -161,7 +161,7 @@ theorem mem_orthogonal_iff {N : Submodule R M} {m : M} :
 theorem orthogonal_le (h : N ≤ L) : B.orthogonal L ≤ B.orthogonal N := fun _ hn l hl => hn l (h hl)
 #align bilin_form.orthogonal_le BilinForm.orthogonal_le
 
-theorem le_orthogonal_orthogonal (b : B.IsRefl) : N ≤ B.orthogonal (B.orthogonal N) :=
+theorem le_orthogonal_orthogonal (b : B₂.IsRefl) : N₂ ≤ B₂.orthogonal (B₂.orthogonal N₂) :=
   fun n hn _ hm => b _ _ (hm n hn)
 #align bilin_form.le_orthogonal_orthogonal BilinForm.le_orthogonal_orthogonal
 
@@ -214,10 +214,10 @@ variable [AddCommMonoid M₂'] [Module R M₂']
 
 /-- The restriction of a reflexive bilinear form `B` onto a submodule `W` is
 nondegenerate if `Disjoint W (B.orthogonal W)`. -/
-theorem nondegenerateRestrictOfDisjointOrthogonal (B : BilinForm R₁ M₁) (b : B.IsRefl)
-    {W : Submodule R₁ M₁} (hW : Disjoint W (B.orthogonal W)) : (B.restrict W).Nondegenerate := by
+theorem nondegenerateRestrictOfDisjointOrthogonal (B : BilinForm R₃ M₃) (b : B.IsRefl)
+    {W : Submodule R₃ M₃} (hW : Disjoint W (B.orthogonal W)) : (B.restrict W).Nondegenerate := by
   rintro ⟨x, hx⟩ b₁
-  rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R₁]
+  rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R₃]
   refine' hW.le_bot ⟨hx, fun y hy => _⟩
   specialize b₁ ⟨y, hy⟩
   rw [restrict_apply, Submodule.coe_mk, Submodule.coe_mk] at b₁

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -42,7 +42,6 @@
 variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V]
 variable {M' M'' : Type*}
 variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M'']
-
 variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁}
 
 namespace BilinForm
@@ -51,18 +50,18 @@
 
 
 /-- The proposition that a bilinear form is reflexive -/
-def IsRefl (B : BilinForm R M) : Prop :=
-  ∀ x y : M, B x y = 0 → B y x = 0
+def IsRefl (B : BilinForm R₂ M₂) : Prop :=
+  ∀ x y : M₂, B x y = 0 → B y x = 0
 #align bilin_form.is_refl BilinForm.IsRefl
 
 namespace IsRefl
 
-variable (H : B.IsRefl)
+variable (H : B₂.IsRefl)
 
-theorem eq_zero : ∀ {x y : M}, B x y = 0 → B y x = 0 := fun {x y} => H x y
+theorem eq_zero : ∀ {x y : M₂}, B₂ x y = 0 → B₂ y x = 0 := fun {x y} => H x y
 #align bilin_form.is_refl.eq_zero BilinForm.IsRefl.eq_zero
 
-protected theorem neg {B : BilinForm R₁ M₁} (hB : B.IsRefl) : (-B).IsRefl := fun x y =>
+protected theorem neg {B : BilinForm R₃ M₃} (hB : B.IsRefl) : (-B).IsRefl := fun x y =>
   neg_eq_zero.mpr ∘ hB x y ∘ neg_eq_zero.mp
 #align bilin_form.is_refl.neg BilinForm.IsRefl.neg
 
@@ -73,68 +72,68 @@
     smul_eq_zero_of_right _ (hB _ _ hBz)
 #align bilin_form.is_refl.smul BilinForm.IsRefl.smul
 
-protected theorem groupSMul {α} [Group α] [DistribMulAction α R] [SMulCommClass α R R] (a : α)
-    {B : BilinForm R M} (hB : B.IsRefl) : (a • B).IsRefl := fun x y =>
+protected theorem groupSMul {α} [Group α] [DistribMulAction α R₂] [SMulCommClass α R₂ R₂] (a : α)
+    {B : BilinForm R₂ M₂} (hB : B.IsRefl) : (a • B).IsRefl := fun x y =>
   (smul_eq_zero_iff_eq _).mpr ∘ hB x y ∘ (smul_eq_zero_iff_eq _).mp
 #align bilin_form.is_refl.group_smul BilinForm.IsRefl.groupSMul
 
 end IsRefl
 
 @[simp]
-theorem isRefl_zero : (0 : BilinForm R M).IsRefl := fun _ _ _ => rfl
+theorem isRefl_zero : (0 : BilinForm R₂ M₂).IsRefl := fun _ _ _ => rfl
 #align bilin_form.is_refl_zero BilinForm.isRefl_zero
 
 @[simp]
-theorem isRefl_neg {B : BilinForm R₁ M₁} : (-B).IsRefl ↔ B.IsRefl :=
+theorem isRefl_neg {B : BilinForm R₃ M₃} : (-B).IsRefl ↔ B.IsRefl :=
   ⟨fun h => neg_neg B ▸ h.neg, IsRefl.neg⟩
 #align bilin_form.is_refl_neg BilinForm.isRefl_neg
 
 /-- The proposition that a bilinear form is symmetric -/
-def IsSymm (B : BilinForm R M) : Prop :=
-  ∀ x y : M, B x y = B y x
+def IsSymm (B : BilinForm R₂ M₂) : Prop :=
+  ∀ x y : M₂, B x y = B y x
 #align bilin_form.is_symm BilinForm.IsSymm
 
 namespace IsSymm
 
-variable (H : B.IsSymm)
+variable (H : B₂.IsSymm)
 
-protected theorem eq (x y : M) : B x y = B y x :=
+protected theorem eq (x y : M₂) : B₂ x y = B₂ y x :=
   H x y
 #align bilin_form.is_symm.eq BilinForm.IsSymm.eq
 
-theorem isRefl : B.IsRefl := fun x y H1 => H x y ▸ H1
+theorem isRefl : B₂.IsRefl := fun x y H1 => H x y ▸ H1
 #align bilin_form.is_symm.is_refl BilinForm.IsSymm.isRefl
 
-protected theorem add {B₁ B₂ : BilinForm R M} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
+protected theorem add {B₁ B₂ : BilinForm R₂ M₂} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
     (B₁ + B₂).IsSymm := fun x y => (congr_arg₂ (· + ·) (hB₁ x y) (hB₂ x y) : _)
 #align bilin_form.is_symm.add BilinForm.IsSymm.add
 
-protected theorem sub {B₁ B₂ : BilinForm R₁ M₁} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
+protected theorem sub {B₁ B₂ : BilinForm R₃ M₃} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
     (B₁ - B₂).IsSymm := fun x y => (congr_arg₂ Sub.sub (hB₁ x y) (hB₂ x y) : _)
 #align bilin_form.is_symm.sub BilinForm.IsSymm.sub
 
-protected theorem neg {B : BilinForm R₁ M₁} (hB : B.IsSymm) : (-B).IsSymm := fun x y =>
+protected theorem neg {B : BilinForm R₃ M₃} (hB : B.IsSymm) : (-B).IsSymm := fun x y =>
   congr_arg Neg.neg (hB x y)
 #align bilin_form.is_symm.neg BilinForm.IsSymm.neg
 
-protected theorem smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R R] (a : α)
-    {B : BilinForm R M} (hB : B.IsSymm) : (a • B).IsSymm := fun x y =>
+protected theorem smul {α} [Monoid α] [DistribMulAction α R₂] [SMulCommClass α R₂ R₂] (a : α)
+    {B : BilinForm R₂ M₂} (hB : B.IsSymm) : (a • B).IsSymm := fun x y =>
   congr_arg (a • ·) (hB x y)
 #align bilin_form.is_symm.smul BilinForm.IsSymm.smul
 
 /-- The restriction of a symmetric bilinear form on a submodule is also symmetric. -/
-theorem restrict {B : BilinForm R M} (b : B.IsSymm) (W : Submodule R M) :
+theorem restrict {B : BilinForm R₂ M₂} (b : B.IsSymm) (W : Submodule R₂ M₂) :
     (B.restrict W).IsSymm := fun x y => b x y
 #align bilin_form.restrict_symm BilinForm.IsSymm.restrict
 
 end IsSymm
 
 @[simp]
-theorem isSymm_zero : (0 : BilinForm R M).IsSymm := fun _ _ => rfl
+theorem isSymm_zero : (0 : BilinForm R₂ M₂).IsSymm := fun _ _ => rfl
 #align bilin_form.is_symm_zero BilinForm.isSymm_zero
 
 @[simp]
-theorem isSymm_neg {B : BilinForm R₁ M₁} : (-B).IsSymm ↔ B.IsSymm :=
+theorem isSymm_neg {B : BilinForm R₃ M₃} : (-B).IsSymm ↔ B.IsSymm :=
   ⟨fun h => neg_neg B ▸ h.neg, IsSymm.neg⟩
 #align bilin_form.is_symm_neg BilinForm.isSymm_neg
 
@@ -161,7 +160,7 @@
   exact H1
 #align bilin_form.is_alt.neg_eq BilinForm.IsAlt.neg_eq
 
-theorem isRefl (H : B₁.IsAlt) : B₁.IsRefl := by
+theorem isRefl (H : B₃.IsAlt) : B₃.IsRefl := by
   intro x y h
   rw [← neg_eq H, h, neg_zero]
 #align bilin_form.is_alt.is_refl BilinForm.IsAlt.isRefl