Commit 2025-05-20 13:01 923a83b2

View on Github →

feat(Matroid/Rank): finish ENat rank API (#24974) This small PR includes the last few lemmas in the API about ENat-valued matroid rank.

Estimated changes

Modified Mathlib/Data/Matroid/Rank/ENat.lean

added theorem Matroid.Spanning.eRank_restrict

added theorem Matroid.Spanning.eRk_eq

modified theorem Matroid.eRank_emptyOn

modified theorem Matroid.eRank_freeOn

added theorem Matroid.eRank_lt_top_iff

added theorem Matroid.eRk_loops

added theorem Matroid.spanning_iff_eRk_le'

added theorem Matroid.spanning_iff_eRk_le