From b22d8c0b1b1d782931caead2529a876bd56b500a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 02:49:52 +0000 Subject: [PATCH] chore(LinearAlgebra/Matrix/Nondegenerate): generalize lemmas to CommSemiring Co-Authored-By: Claude Opus 4.8 (1M context) --- Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean b/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean index ef2b5bee37197c..3a8f262c4f5e2f 100644 --- a/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean +++ b/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean @@ -46,7 +46,9 @@ structure Nondegenerate (M : Matrix m n R) : Prop where end Finite -variable {m n R : Type*} [CommRing R] {M : Matrix m n R} +section CommSemiring + +variable {m n R : Type*} [CommSemiring R] {M : Matrix m n R} lemma separatingRight_def [Fintype m] [Fintype n] : M.SeparatingRight ↔ (∀ w, (∀ v, v ⬝ᵥ M *ᵥ w = 0) → w = 0) := by @@ -61,9 +63,7 @@ lemma separatingLeft_def [Fintype m] [Fintype n] : 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⟩ + rw [nondegenerate_iff, separatingLeft_def, separatingRight_def] theorem separatingLeft_iff_forall_vecMul_eq_zero [Fintype m] [Finite n] : M.SeparatingLeft ↔ ∀ v, v ᵥ* M = 0 → v = 0 := by @@ -140,8 +140,10 @@ theorem Nondegenerate.exists_not_ortho_of_ne_zero' (hM : Nondegenerate M) {w : n ∃ v, v ⬝ᵥ M *ᵥ w ≠ 0 := not_forall.mp (mt hM.eq_zero_of_ortho' hw) +end CommSemiring + section Determinant -variable [DecidableEq m] {M : Matrix m m R} +variable {m R : Type*} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} open scoped nonZeroDivisors