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.