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.