Theorem Matroid.Indep.cardinalMk_le_basis'_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.Indep.cardinalMk_le_basis'_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.Indep.cardinalMk_le_basis'_of_finitaryView on Github →