Theorem Matroid.Basis'.cardinalMk_eq_of_finitary

Modification history

2025-01-27 23:15
Mathlib/Data/Matroid/Rank/Cardinal.lean
feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) …
Deleted Matroid.Basis'.cardinalMk_eq_of_finitaryView on Github →
2025-01-21 11:45
Mathlib/Data/Matroid/Rank/Cardinal.lean
feat(Matroid): all bases of a finitary matroid have the same cardinality (#20888)
Added Matroid.Basis'.cardinalMk_eq_of_finitaryView on Github →