Commit 2025-01-21 11:45 c499ecfa

View on Github →

feat(Matroid): all bases of a finitary matroid have the same cardinality (#20888)

Estimated changes

Modified Mathlib.lean

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

added theorem Matroid.Base.cardinalMk_diff_comm_of_finitary

added theorem Matroid.Base.cardinalMk_eq_of_finitary

added theorem Matroid.Basis'.cardinalMk_diff_comm_of_finitary

added theorem Matroid.Basis'.cardinalMk_eq_of_finitary

added theorem Matroid.Basis.cardinalMk_diff_comm_of_finitary

added theorem Matroid.Basis.cardinalMk_eq_of_finitary

added theorem Matroid.Indep.cardinalMk_le_base_of_finitary

added theorem Matroid.Indep.cardinalMk_le_basis'_of_finitary

added theorem Matroid.Indep.cardinalMk_le_basis_of_finitary