Commit 2026-07-01 17:54 b49d30f6

feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains (#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 NonUnitalNonAssocSemirings in the defs