Commit 2025-02-10 21:55 2336f1b6

View on Github →

feat(Matroid): cardinality criteria for indep/spanning sets to be bases (#21512)

Estimated changes

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.Base.eq_of_superset_spanning

added theorem Matroid.Spanning.base_of_minimal

added theorem Matroid.base_iff_minimal_spanning

added theorem Matroid.flat_closure

added theorem Matroid.flat_iff_closure_eq

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

added theorem Matroid.Indep.base_of_cRank_le

added theorem Matroid.Indep.base_of_cRank_le_of_finite

added theorem Matroid.Indep.cardinalMk_le_cRank

added theorem Matroid.Spanning.base_of_le_cRank

added theorem Matroid.Spanning.base_of_le_cRank_of_finite

added theorem Matroid.Spanning.cRank_le_cardinalMk

added theorem Matroid.cRank_eq_iSup_cardinalMk_indep

added theorem Matroid.rankFinite_iff_cRank_lt_aleph0