Theorem Module.le_rank_iff_exists_linearMap

Modification history

2025-11-28 14:12
Mathlib/LinearAlgebra/Dimension/Basic.lean
feat(LinearAlgebra): rank of commutative semiring over itself (#32123)
Added Module.le_rank_iff_exists_linearMapView on Github →