Commit 2025-05-09 11:08 faf08141

View on Github →

chore(LinearAlgebra): generalize some lemmas (#23729) and move them to earlier files. rank_subsingleton', rank_punit and rank_bot are generalized from Ring to Semiring. linearIndependent_subsingleton_iff is generalized to Semiring and an extraneous NoZeroSMulDivisors condition is removed. ENat.card_ne_zero_iff_nonempty is added.

Estimated changes