Commit 2025-01-27 23:15 d66fa49e

View on Github →

feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) We abstract out the matroid property of 'having a well-defined Cardinality-valued rank function' as a typeclass Matroid.CardinalRank, and use it to define a rank function Matroid.cardRk and prove basic properties. The fact that Finitary matroids have such a rank function is now provided as an instance.

Estimated changes

Modified Mathlib/Data/Matroid/Basic.lean

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

added theorem Matroid.Base.cardinalMk_diff_comm

deleted theorem Matroid.Base.cardinalMk_diff_comm_of_finitary

added theorem Matroid.Base.cardinalMk_eq

added theorem Matroid.Base.cardinalMk_eq_cRank

deleted theorem Matroid.Base.cardinalMk_eq_of_finitary

added theorem Matroid.Base.cardinalMk_le_cRank

added theorem Matroid.Basis'.cardinalMk_diff_comm

deleted theorem Matroid.Basis'.cardinalMk_diff_comm_of_finitary

added theorem Matroid.Basis'.cardinalMk_eq

added theorem Matroid.Basis'.cardinalMk_eq_cRk

deleted theorem Matroid.Basis'.cardinalMk_eq_of_finitary

added theorem Matroid.Basis'.cardinalMk_le_cRk

added theorem Matroid.Basis.cardinalMk_diff_comm

deleted theorem Matroid.Basis.cardinalMk_diff_comm_of_finitary

added theorem Matroid.Basis.cardinalMk_eq

added theorem Matroid.Basis.cardinalMk_eq_cRk

deleted theorem Matroid.Basis.cardinalMk_eq_of_finitary

added theorem Matroid.Basis.cardinalMk_le_cRk

added theorem Matroid.Indep.cRk_eq_cardinalMk

added theorem Matroid.Indep.cardinalMk_le_base

deleted theorem Matroid.Indep.cardinalMk_le_base_of_finitary

added theorem Matroid.Indep.cardinalMk_le_basis'

deleted theorem Matroid.Indep.cardinalMk_le_basis'_of_finitary

added theorem Matroid.Indep.cardinalMk_le_basis

deleted theorem Matroid.Indep.cardinalMk_le_basis_of_finitary

added theorem Matroid.Indep.cardinalMk_le_cRk_of_subset

added theorem Matroid.cRank_le_iff

added theorem Matroid.cRank_restrict

added theorem Matroid.cRk_closure

added theorem Matroid.cRk_closure_congr

added theorem Matroid.cRk_comap

added theorem Matroid.cRk_comap_lift

added theorem Matroid.cRk_ground

added theorem Matroid.cRk_insert_closure_eq

added theorem Matroid.cRk_inter_add_cRk_union_le

added theorem Matroid.cRk_inter_ground

added theorem Matroid.cRk_le_cardinalMk

added theorem Matroid.cRk_le_iff

added theorem Matroid.cRk_le_of_subset

added theorem Matroid.cRk_map_eq

added theorem Matroid.cRk_map_image

added theorem Matroid.cRk_map_image_lift

added theorem Matroid.cRk_mono

added theorem Matroid.cRk_restrict

added theorem Matroid.cRk_restrict_subset

added theorem Matroid.cRk_union_closure_eq

added theorem Matroid.cRk_union_closure_left_eq

added theorem Matroid.cRk_union_closure_right_eq