Commit 2025-11-28 14:12 b7da4190

View on Github →

feat(LinearAlgebra): rank of commutative semiring over itself (#32123)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

added theorem CommSemiring.rank_self

added theorem Module.le_rank_iff

added theorem Module.le_rank_iff_exists_finset

added theorem Module.le_rank_iff_exists_linearMap

added theorem Module.one_le_rank_iff

added theorem rank_subsingleton

Modified Mathlib/LinearAlgebra/Dimension/Finrank.lean

added theorem CommSemiring.finrank_self

Modified Mathlib/LinearAlgebra/Dimension/Subsingleton.lean

deleted theorem rank_subsingleton

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.exists_finset_eq_card