feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341)

Lemma `is_refl` shows that an alternating sesquilinear form is reflexive.
Refactored `sesquilinear_form` in a similar way as `bilinear_form` will be in #10338.

Author: mcdoll

src/linear_algebra/sesquilinear_form.lean

@@ -262,60 +262,44 @@ end
 
 end is_domain
 
-end sesq_form
-
-namespace refl_sesq_form
-
-open refl_sesq_form sesq_form
-
 variables {R : Type*} {M : Type*} [ring R] [add_comm_group M] [module R M]
 variables {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I}
 
 /-- The proposition that a sesquilinear form is reflexive -/
 def is_refl (S : sesq_form R M I) : Prop := ∀ (x y : M), S x y = 0 → S y x = 0
 
-variable (H : is_refl S)
-
-lemma eq_zero : ∀ {x y : M}, S x y = 0 → S y x = 0 := λ x y, H x y
-
-lemma ortho_sym {x y : M} :
-is_ortho S x y ↔ is_ortho S y x := ⟨eq_zero H, eq_zero H⟩
+namespace is_refl
 
-end refl_sesq_form
+variable (H : S.is_refl)
 
-namespace sym_sesq_form
+lemma eq_zero : ∀ {x y : M}, S x y = 0 → S y x = 0 := λ x y, H x y
 
-open sym_sesq_form sesq_form
+lemma ortho_comm {x y : M} : is_ortho S x y ↔ is_ortho S y x := ⟨eq_zero H, eq_zero H⟩
 
-variables {R : Type*} {M : Type*} [ring R] [add_comm_group M] [module R M]
-variables {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I}
+end is_refl
 
 /-- The proposition that a sesquilinear form is symmetric -/
-def is_sym (S : sesq_form R M I) : Prop := ∀ (x y : M), (I (S x y)).unop = S y x
-
-variable (H : is_sym S)
-include H
+def is_symm (S : sesq_form R M I) : Prop := ∀ (x y : M), (I (S x y)).unop = S y x
 
-lemma sym (x y : M) : (I (S x y)).unop = S y x := H x y
+namespace is_symm
 
-lemma is_refl : refl_sesq_form.is_refl S := λ x y H1, by { rw [←H], simp [H1], }
-
-lemma ortho_sym {x y : M} :
-is_ortho S x y ↔ is_ortho S y x := refl_sesq_form.ortho_sym (is_refl H)
+variable (H : S.is_symm)
+include H
 
-end sym_sesq_form
+protected lemma eq (x y : M) : (I (S x y)).unop = S y x := H x y
 
-namespace alt_sesq_form
+lemma is_refl : S.is_refl := λ x y H1, by { rw [←H], simp [H1], }
 
-open alt_sesq_form sesq_form
+lemma ortho_comm {x y : M} : is_ortho S x y ↔ is_ortho S y x := H.is_refl.ortho_comm
 
-variables {R : Type*} {M : Type*} [ring R] [add_comm_group M] [module R M]
-variables {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I}
+end is_symm
 
 /-- The proposition that a sesquilinear form is alternating -/
 def is_alt (S : sesq_form R M I) : Prop := ∀ (x : M), S x x = 0
 
-variable (H : is_alt S)
+namespace is_alt
+
+variable (H : S.is_alt)
 include H
 
 lemma self_eq_zero (x : M) : S x x = 0 := H x
@@ -331,4 +315,14 @@ begin
   exact H1,
 end
 
-end alt_sesq_form
+lemma is_refl : S.is_refl :=
+begin
+  intros x y h,
+  rw [← neg H, h, neg_zero],
+end
+
+lemma ortho_comm {x y : M} : is_ortho S x y ↔ is_ortho S y x := H.is_refl.ortho_comm
+
+end is_alt
+
+end sesq_form