Commit 2025-02-09 22:17 a443ebbe

View on Github →

chore(Matroid): rename Rk -> Rank in typeclass names (#21605) as per the (weak) consensus on zulip and the convention established in Data.Matroid.Rank.Cardinal, the rank of a matroid is referred to as 'rank' in lemma names, and the rank of a set is referred to as rk. Accordingly (and for internal consistency), we rename the typeclasses RkPos -> RankPos, FiniteRk -> RankFinite and InfiniteRk -> RankInfinite.

Estimated changes

modified theorem Matroid.Base.finite
modified theorem Matroid.Base.infinite
modified theorem Matroid.Base.nonempty
modified theorem Matroid.Basis.Finite
modified theorem Matroid.Indep.finite
modified theorem Matroid.empty_not_base
deleted theorem Matroid.not_finiteRk
deleted theorem Matroid.not_infiniteRk
added theorem Matroid.not_rankFinite
added theorem Matroid.freeOn_rankPos
deleted theorem Matroid.freeOn_rkPos
deleted theorem Matroid.not_rkPos_iff
modified theorem Matroid.Base.ssubset_ground
modified theorem Matroid.ground_not_base