chore(LinearAlgebra/Matrix/Nondegenerate): generalize lemmas to CommSemiring (leanprover-community#41271)

This PR generalizes the `SeparatingLeft`/`SeparatingRight`/`Nondegenerate` lemmas from `CommRing` to `CommSemiring` (the determinant section keeps `CommRing`), and golfs `nondegenerate_def` using the `@[mk_iff]`-generated `nondegenerate_iff`. Follow-up to leanprover-community#39634, which generalized the definitions but left the lemmas at `CommRing`.

🤖 Prepared with Claude Code

Author: kim-em

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