Commit 2025-05-05 14:12 88984e55

View on Github →

feat(Matroid/Rank): more rank API (#23951) We add some more API for matroid rank and its interactions with monotonicity, duality, finiteness and submodularity.

Estimated changes

modified theorem Matroid.eRank_emptyOn
modified theorem Matroid.eRank_eq_top
added theorem Matroid.eRank_freeOn
modified theorem Matroid.eRank_loopyOn
modified theorem Matroid.eRank_map
added theorem Matroid.eRk_comap
deleted theorem Matroid.eRk_comap_eq
added theorem Matroid.eRk_eq_top_iff
added theorem Matroid.eRk_freeOn
added theorem Matroid.eRk_loopyOn
added theorem Matroid.eRk_lt_top_iff
added theorem Matroid.eRk_map
deleted theorem Matroid.eRk_map_eq
added theorem Matroid.eRk_ne_top_iff