feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains (leanprover-community#39634)

- Syntactically generalize the bilinear form identities to non-square matrices
- Prove iff and transpose theorems for `SeparatingLeft`/`SeparatingRight`/`Nondegenerate`
- Prove `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` given `Nondegenerate`
  (extracted from the existing `eq_zero_of_*_eq_zero`)
- Generalize `M.det ≠ 0 → M.Nondegenerate` to `M.det ∈ R⁰ → M.Nondegenerate` (over any `CommRing`)
- Add `M *ᵥ v = 0 → v = 0` and `v ᵥ* M = 0 → v = 0` theorems given `M.det ∈ R⁰`
- Allow `NonUnitalNonAssocSemiring`s in the `def`s

Author: SnirBroshi

Mathlib/Data/Matrix/Mul.lean

@@ -1093,13 +1093,13 @@ theorem vecMul_transpose [Fintype n] (A : Matrix m n α) (x : n → α) : x ᵥ*
   apply dotProduct_comm
 
 /-- Bilinear form identity: `x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x` for commutative semirings. -/
-theorem dotProduct_transpose_mulVec [Fintype m] (A : Matrix m m α) (x y : m → α) :
-    x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x := by
+theorem dotProduct_transpose_mulVec [Fintype m] [Fintype n] (A : Matrix m n α) (x : n → α)
+    (y : m → α) : x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x := by
   rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]
 
 /-- Bilinear form identity: `(x ᵥ* Aᵀ) ⬝ᵥ y = (y ᵥ* A) ⬝ᵥ x` for commutative semirings. -/
-theorem dotProduct_vecMul_transpose [Fintype m] (A : Matrix m m α) (x y : m → α) :
-    (x ᵥ* Aᵀ) ⬝ᵥ y = (y ᵥ* A) ⬝ᵥ x := by
+theorem dotProduct_vecMul_transpose [Fintype m] [Fintype n] (A : Matrix m n α) (x : n → α)
+    (y : m → α) : (x ᵥ* Aᵀ) ⬝ᵥ y = (y ᵥ* A) ⬝ᵥ x := by
   simpa [dotProduct_mulVec] using dotProduct_transpose_mulVec (A := A) (x := x) (y := y)
 
 theorem mulVec_vecMul [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) :

Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

@@ -26,7 +26,7 @@ namespace Matrix
 
 section Finite
 
-variable {m n R A : Type*} [CommRing R] [Finite m] [Finite n] (M : Matrix m n R)
+variable {m n R A : Type*} [NonUnitalNonAssocSemiring R] [Finite m] [Finite n] (M : Matrix m n R)
 
 attribute [local instance] Fintype.ofFinite
 
@@ -39,29 +39,87 @@ def SeparatingLeft : Prop :=
   (∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0)
 
 /-- A matrix `M` is nondegenerate if it is both left-separating and right-separating. -/
+@[mk_iff]
 structure Nondegenerate (M : Matrix m n R) : Prop where
   separatingLeft : SeparatingLeft M
   separatingRight : SeparatingRight M
 
 end Finite
 
-variable {m n R A : Type*} [CommRing R] [Fintype m] [Fintype n] [CommRing A] [IsDomain A]
-  {M : Matrix m n R}
+variable {m n R : Type*} [CommRing R] {M : Matrix m n R}
 
-lemma separatingRight_def : M.SeparatingRight ↔ (∀ w, (∀ v, v ⬝ᵥ M *ᵥ w = 0) → w = 0) := by
+lemma separatingRight_def [Fintype m] [Fintype n] :
+    M.SeparatingRight ↔ (∀ w, (∀ v, v ⬝ᵥ M *ᵥ w = 0) → w = 0) := by
   refine forall_congr' fun w ↦ ⟨fun hM hw ↦ hM ?_, fun hM hw ↦ hM ?_⟩ <;>
   convert! hw
 
-lemma separatingLeft_def : M.SeparatingLeft ↔ (∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0) := by
+lemma separatingLeft_def [Fintype m] [Fintype n] :
+    M.SeparatingLeft ↔ (∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0) := by
   refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩ <;>
   convert! hv
 
-lemma nondegenerate_def : M.Nondegenerate ↔
-   (∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ (∀ w, (∀ v, v ⬝ᵥ M *ᵥ w = 0) → w = 0) := by
+lemma nondegenerate_def [Fintype m] [Fintype n] :
+    M.Nondegenerate ↔
+      (∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ (∀ w, (∀ v, v ⬝ᵥ M *ᵥ w = 0) → w = 0) := by
   constructor
   · exact fun h ↦ ⟨separatingLeft_def.mp h.1, separatingRight_def.mp h.2⟩
   · exact fun h ↦ ⟨separatingLeft_def.mpr h.1, separatingRight_def.mpr h.2⟩
 
+theorem separatingLeft_iff_forall_vecMul_eq_zero [Fintype m] [Finite n] :
+    M.SeparatingLeft ↔ ∀ v, v ᵥ* M = 0 → v = 0 := by
+  have := Fintype.ofFinite n
+  rw [separatingLeft_def]
+  refine ⟨fun h v hv ↦ h v fun w ↦ ?_, fun h w hw ↦ h w <| funext fun i ↦ ?_⟩
+  · simp [dotProduct_mulVec, hv]
+  · classical simpa using! hw <| Pi.single i 1
+
+theorem separatingRight_iff_forall_mulVec_eq_zero [Finite m] [Fintype n] :
+    M.SeparatingRight ↔ ∀ v, M *ᵥ v = 0 → v = 0 := by
+  have := Fintype.ofFinite m
+  rw [separatingRight_def]
+  refine ⟨fun h v hv ↦ h v fun w ↦ ?_, fun h w hw ↦ h w <| funext fun i ↦ ?_⟩
+  · simp [hv]
+  · classical simpa using hw <| Pi.single i 1
+
+theorem SeparatingLeft.eq_zero_of_vecMul_eq_zero [Fintype m] [Finite n] (hM : M.SeparatingLeft)
+    {v : m → R} (hv : v ᵥ* M = 0) : v = 0 :=
+  separatingLeft_iff_forall_vecMul_eq_zero.mp hM v hv
+
+theorem SeparatingRight.eq_zero_of_mulVec_eq_zero [Finite m] [Fintype n] (hM : M.SeparatingRight)
+    {v : n → R} (hv : M *ᵥ v = 0) : v = 0 :=
+  separatingRight_iff_forall_mulVec_eq_zero.mp hM v hv
+
+theorem nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero [Fintype m] [Fintype n] :
+    M.Nondegenerate ↔ (∀ v, v ᵥ* M = 0 → v = 0) ∧ (∀ v, M *ᵥ v = 0 → v = 0) := by
+  rw [nondegenerate_iff, separatingLeft_iff_forall_vecMul_eq_zero,
+    separatingRight_iff_forall_mulVec_eq_zero]
+
+@[simp]
+theorem separatingLeft_transpose_iff [Finite m] [Finite n] :
+    Mᵀ.SeparatingLeft ↔ M.SeparatingRight := by
+  have := Fintype.ofFinite m
+  have := Fintype.ofFinite n
+  simp_rw [separatingLeft_def, separatingRight_def, dotProduct_transpose_mulVec]
+
+alias ⟨_, SeparatingRight.separatingLeft_transpose⟩ := separatingLeft_transpose_iff
+
+@[simp]
+theorem separatingRight_transpose_iff [Finite m] [Finite n] :
+    Mᵀ.SeparatingRight ↔ M.SeparatingLeft := by
+  have := Fintype.ofFinite m
+  have := Fintype.ofFinite n
+  simp_rw [separatingRight_def, separatingLeft_def, dotProduct_transpose_mulVec]
+
+alias ⟨_, SeparatingLeft.separatingRight_transpose⟩ := separatingRight_transpose_iff
+
+@[simp]
+theorem nondegenerate_transpose_iff [Finite m] [Finite n] : Mᵀ.Nondegenerate ↔ M.Nondegenerate := by
+  simp [nondegenerate_iff, and_comm]
+
+alias ⟨_, Nondegenerate.transpose⟩ := nondegenerate_transpose_iff
+
+variable [Fintype m] [Fintype n]
+
 /-- If `M` is nondegenerate and `w * M * v = 0` for all `w`, then `v = 0`. -/
 theorem Nondegenerate.eq_zero_of_ortho (hM : Nondegenerate M) {v : m → R}
     (hv : ∀ w, v ⬝ᵥ M *ᵥ w = 0) : v = 0 :=
@@ -73,42 +131,51 @@ theorem Nondegenerate.exists_not_ortho_of_ne_zero (hM : Nondegenerate M)
   not_forall.mp (mt hM.eq_zero_of_ortho hv)
 
 /-- If `M` is nondegenerate and `w * M * v = 0` for all `v`, then `w = 0`. -/
-theorem Nondegenerate.eq_zero_of_ortho' {M : Matrix m n R} (hM : Nondegenerate M) {w : n → R}
+theorem Nondegenerate.eq_zero_of_ortho' (hM : Nondegenerate M) {w : n → R}
     (hw : ∀ v, v ⬝ᵥ M *ᵥ w = 0) : w = 0 :=
   (nondegenerate_def.mp hM).2 w hw
 
 /-- If `M` is nondegenerate and `w ≠ 0`, then there is some `v` such that `v * M * w ≠ 0`. -/
-theorem Nondegenerate.exists_not_ortho_of_ne_zero' {M : Matrix m n R} (hM : Nondegenerate M)
-    {w : n → R} (hw : w ≠ 0) : ∃ v, v ⬝ᵥ M *ᵥ w ≠ 0 :=
+theorem Nondegenerate.exists_not_ortho_of_ne_zero' (hM : Nondegenerate M) {w : n → R} (hw : w ≠ 0) :
+    ∃ v, v ⬝ᵥ M *ᵥ w ≠ 0 :=
   not_forall.mp (mt hM.eq_zero_of_ortho' hw)
 
 section Determinant
-variable [DecidableEq m] {M : Matrix m m A}
+variable [DecidableEq m] {M : Matrix m m R}
+
+open scoped nonZeroDivisors
+
+private theorem SeparatingLeft.of_det_mem_nonZeroDivisors (hM : M.det ∈ R⁰) : M.SeparatingLeft := by
+  refine separatingLeft_def.mpr fun v h ↦ funext fun i ↦ mem_nonZeroDivisors_iff_left.mp hM _ ?_
+  simpa using h <| M.cramer <| Pi.single i 1
+
+theorem Nondegenerate.of_det_mem_nonZeroDivisors (hM : M.det ∈ R⁰) : M.Nondegenerate where
+  separatingLeft := .of_det_mem_nonZeroDivisors hM
+  separatingRight := separatingLeft_transpose_iff.mp <| .of_det_mem_nonZeroDivisors <| by simpa
 
-/-- If `M` is square and has nonzero determinant, then `M` as a bilinear form on `n → A` is
+/-- If `M` is square and has nonzero determinant, then `M` as a bilinear form on `n → R` is
 nondegenerate. The "iff" implication, `nondegenerate_iff_det_ne_zero`, is proved in a later file.
 
 See also `BilinForm.nondegenerateOfDetNeZero'` and `BilinForm.nondegenerateOfDetNeZero`.
 -/
-theorem nondegenerate_of_det_ne_zero (hM : M.det ≠ 0) : Nondegenerate M := by
-  refine nondegenerate_def.mpr ⟨fun v h ↦ ?_, fun w h ↦ ?_⟩
-  · ext i
-    specialize h (M.cramer (Pi.single i 1))
-    simp_all
-  · ext i
-    contrapose! h
-    use Pi.single i 1 ᵥ* M.adjugate
-    rw [dotProduct_mulVec, vecMul_vecMul, adjugate_mul]
-    simp_all [dotProduct, smul_apply, smul_eq_mul, Matrix.one_apply]
-
-theorem eq_zero_of_vecMul_eq_zero (hM : M.det ≠ 0) {v : m → A}
+theorem nondegenerate_of_det_ne_zero [NoZeroDivisors R] (hM : M.det ≠ 0) : M.Nondegenerate :=
+  .of_det_mem_nonZeroDivisors <| mem_nonZeroDivisors_of_ne_zero hM
+
+theorem eq_zero_of_det_mem_nonZeroDivisors_of_vecMul_eq_zero (hM : M.det ∈ R⁰)
+    {v : m → R} (hv : v ᵥ* M = 0) : v = 0 :=
+  Nondegenerate.of_det_mem_nonZeroDivisors hM |>.separatingLeft.eq_zero_of_vecMul_eq_zero hv
+
+theorem eq_zero_of_vecMul_eq_zero [NoZeroDivisors R] (hM : M.det ≠ 0) {v : m → R}
     (hv : v ᵥ* M = 0) : v = 0 :=
-  (nondegenerate_of_det_ne_zero hM).eq_zero_of_ortho fun w => by
-    rw [dotProduct_mulVec, hv, zero_dotProduct]
+  nondegenerate_of_det_ne_zero hM |>.separatingLeft.eq_zero_of_vecMul_eq_zero hv
+
+theorem eq_zero_of_det_mem_nonZeroDivisors_of_mulVec_eq_zero (hM : M.det ∈ R⁰)
+    {v : m → R} (hv : M *ᵥ v = 0) : v = 0 :=
+  Nondegenerate.of_det_mem_nonZeroDivisors hM |>.separatingRight.eq_zero_of_mulVec_eq_zero hv
 
-theorem eq_zero_of_mulVec_eq_zero (hM : M.det ≠ 0) {v : m → A}
+theorem eq_zero_of_mulVec_eq_zero [NoZeroDivisors R] (hM : M.det ≠ 0) {v : m → R}
     (hv : M *ᵥ v = 0) : v = 0 :=
-  eq_zero_of_vecMul_eq_zero (by rwa [det_transpose]) ((vecMul_transpose M v).trans hv)
+  nondegenerate_of_det_ne_zero hM |>.separatingRight.eq_zero_of_mulVec_eq_zero hv
 
 end Determinant
 

Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

@@ -158,54 +158,61 @@ private theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq
           RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
       · rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
 
-theorem exists_mulVec_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 :=
+variable {A : Type*} [CommRing A] [IsDomain A] {M N : Matrix n n A}
+
+theorem exists_mulVec_eq_zero_iff [DecidableEq n] : (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 :=
   exists_mulVec_eq_zero_iff' (FractionRing A)
 
-theorem exists_vecMul_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : (∃ v ≠ 0, v ᵥ* M = 0) ↔ M.det = 0 := by
+theorem exists_vecMul_eq_zero_iff [DecidableEq n] : (∃ v ≠ 0, v ᵥ* M = 0) ↔ M.det = 0 := by
   simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff
 
-theorem nondegenerate_iff_det_ne_zero {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : Nondegenerate M ↔ M.det ≠ 0 := by
-  refine ⟨?_, nondegenerate_of_det_ne_zero⟩
-  rw [ne_eq, ← exists_vecMul_eq_zero_iff]
-  push Not
-  intro hM v hv hMv
-  obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv
-  simp [dotProduct_mulVec, hMv, zero_dotProduct, ne_eq] at hwMv
-
-lemma separatingLeft_iff_det_ne_zero {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : SeparatingLeft M ↔ M.det ≠ 0 := by
-  refine ⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).1⟩
-  obtain ⟨v, hvne, hv⟩ := exists_vecMul_eq_zero_iff.mpr hc
-  refine hvne (separatingLeft_def.mp h v ?_)
-  simp [dotProduct_mulVec, hv]
-
-lemma separatingRight_iff_det_ne_zero {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : SeparatingRight M ↔ M.det ≠ 0 := by
-  refine ⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).2⟩
-  obtain ⟨v, hvne, hv⟩ := exists_mulVec_eq_zero_iff.mpr hc
-  refine hvne (separatingRight_def.mp h v ?_)
-  simp [hv]
-
-theorem Nondegenerate.mul_iff_right {A : Type*} [CommRing A] [IsDomain A]
-    {M N : Matrix n n A} (h : N.Nondegenerate) :
+theorem nondegenerate_iff_det_ne_zero [DecidableEq n] : Nondegenerate M ↔ M.det ≠ 0 := by
+  grind [nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero, exists_mulVec_eq_zero_iff,
+    exists_vecMul_eq_zero_iff]
+
+lemma separatingLeft_iff_det_ne_zero [DecidableEq n] : SeparatingLeft M ↔ M.det ≠ 0 := by
+  grind [separatingLeft_iff_forall_vecMul_eq_zero, exists_vecMul_eq_zero_iff]
+
+lemma separatingRight_iff_det_ne_zero [DecidableEq n] : SeparatingRight M ↔ M.det ≠ 0 := by
+  grind [separatingRight_iff_forall_mulVec_eq_zero, exists_mulVec_eq_zero_iff]
+
+omit [Fintype n] in
+theorem nondegenerate_iff_separatingLeft [Finite n] : M.Nondegenerate ↔ M.SeparatingLeft := by
+  classical
+  have := Fintype.ofFinite n
+  rw [nondegenerate_iff_det_ne_zero, separatingLeft_iff_det_ne_zero]
+
+alias ⟨_, SeparatingLeft.nondegenerate⟩ := nondegenerate_iff_separatingLeft
+
+omit [Fintype n] in
+theorem nondegenerate_iff_separatingRight [Finite n] : M.Nondegenerate ↔ M.SeparatingRight := by
+  classical
+  have := Fintype.ofFinite n
+  rw [nondegenerate_iff_det_ne_zero, separatingRight_iff_det_ne_zero]
+
+alias ⟨_, SeparatingRight.nondegenerate⟩ := nondegenerate_iff_separatingRight
+
+omit [Fintype n] in
+theorem separatingLeft_iff_separatingRight [Finite n] : M.SeparatingLeft ↔ M.SeparatingRight :=
+  nondegenerate_iff_separatingLeft.symm.trans nondegenerate_iff_separatingRight
+
+alias ⟨SeparatingLeft.separatingRight, SeparatingRight.separatingLeft⟩ :=
+  separatingLeft_iff_separatingRight
+
+theorem Nondegenerate.mul_iff_right (h : N.Nondegenerate) :
     (M * N).Nondegenerate ↔ M.Nondegenerate := by
   classical
   simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
   exact mul_ne_zero_iff_right h
 
-theorem Nondegenerate.mul_iff_left {A : Type*} [CommRing A] [IsDomain A]
-    {M N : Matrix n n A} (h : M.Nondegenerate) :
+theorem Nondegenerate.mul_iff_left (h : M.Nondegenerate) :
     (M * N).Nondegenerate ↔ N.Nondegenerate := by
   classical
   simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
   exact mul_ne_zero_iff_left h
 
 omit [Fintype n] in
-theorem Nondegenerate.smul_iff [Finite n] {A : Type*} [CommRing A] [IsDomain A]
-    {M : Matrix n n A} {t : A} (h : t ≠ 0) :
+theorem Nondegenerate.smul_iff [Finite n] {t : A} (h : t ≠ 0) :
     (t • M).Nondegenerate ↔ M.Nondegenerate := by
   have := Fintype.ofFinite
   rw [nondegenerate_def, nondegenerate_def]