Theorem Matroid.Indep.cardinalMk_le_cRk_of_subset

Modification history

2025-01-27 23:15
Mathlib/Data/Matroid/Rank/Cardinal.lean
feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) …
Added Matroid.Indep.cardinalMk_le_cRk_of_subsetView on Github →