Commit 2025-02-16 22:38 f8044971

View on Github →

chore(Matroid): add 'Is' to predicate names (#21879) In accordance with emerging guidelines, and to minimize impact on the growing API, we rename Noun-style matroid predicates to IsNoun, deprecating the old names in each case. This includes Base -> IsBase Basis -> IsBasis Basis' -> IsBasis' Circuit -> IsCircuit Flat -> IsFlat Restriction -> IsRestriction.

Estimated changes

deleted theorem Matroid.Base.basis_ground
deleted theorem Matroid.Base.exchange
deleted theorem Matroid.Base.exchange_mem
deleted theorem Matroid.Base.finite
deleted theorem Matroid.Base.indep
deleted theorem Matroid.Base.infinite
deleted theorem Matroid.Base.insert_dep
deleted theorem Matroid.Base.nonempty
deleted theorem Matroid.Basis'.basis
deleted theorem Matroid.Basis'.indep
deleted theorem Matroid.Basis'.subset
deleted def Matroid.Basis'
deleted theorem Matroid.Basis.Finite
deleted theorem Matroid.Basis.basis'
deleted theorem Matroid.Basis.basis_union
deleted theorem Matroid.Basis.exists_base
deleted theorem Matroid.Basis.indep
deleted theorem Matroid.Basis.insert_dep
deleted theorem Matroid.Basis.subset
deleted def Matroid.Basis
deleted theorem Matroid.Indep.basis_self
deleted theorem Matroid.Indep.eq_of_basis
added theorem Matroid.IsBase.finite
added theorem Matroid.IsBase.indep
added theorem Matroid.IsBasis'.indep
added def Matroid.IsBasis'
added theorem Matroid.IsBasis.Finite
added theorem Matroid.IsBasis.indep
added theorem Matroid.IsBasis.subset
added def Matroid.IsBasis
deleted theorem Matroid.basis'_iff_basis
deleted theorem Matroid.basis_empty_iff
deleted theorem Matroid.basis_ground_iff
deleted theorem Matroid.basis_iff'
deleted theorem Matroid.basis_iff
deleted theorem Matroid.basis_iff_maximal
modified def Matroid.copy
modified def Matroid.copyBase
deleted theorem Matroid.empty_not_base
deleted theorem Matroid.exists_basis'
deleted theorem Matroid.exists_basis
added theorem Matroid.exists_isBasis
deleted theorem Matroid.ext_base
deleted theorem Matroid.ext_base_indep
deleted theorem Matroid.ext_iff_base
added theorem Matroid.ext_iff_isBase
added theorem Matroid.ext_isBase
modified theorem Matroid.indep_iff
added theorem Matroid.isBasis_iff'
added theorem Matroid.isBasis_iff
modified theorem Matroid.setOf_indep_eq
deleted theorem Matroid.Circuit.dep
deleted theorem Matroid.Circuit.finite
deleted theorem Matroid.Circuit.minimal
deleted theorem Matroid.Circuit.nonempty
deleted theorem Matroid.Circuit.not_indep
deleted def Matroid.Circuit
added theorem Matroid.IsCircuit.dep
deleted theorem Matroid.circuit_antichain
deleted theorem Matroid.circuit_def
deleted theorem Matroid.circuit_iff
deleted theorem Matroid.empty_not_circuit
deleted theorem Matroid.ext_circuit
deleted theorem Matroid.ext_iff_circuit
added theorem Matroid.ext_isCircuit
added theorem Matroid.isCircuit_def
added theorem Matroid.isCircuit_iff
deleted theorem Matroid.Base.closure_eq
deleted theorem Matroid.Base.spanning
deleted theorem Matroid.Flat.closure
deleted theorem Matroid.Flat.iInter
deleted structure Matroid.Flat
added theorem Matroid.IsFlat.closure
added theorem Matroid.IsFlat.iInter
added structure Matroid.IsFlat
modified def Matroid.closure
modified theorem Matroid.closure_def
deleted theorem Matroid.empty_basis_iff
deleted theorem Matroid.flat_closure
deleted theorem Matroid.flat_iff_isClosed
deleted theorem Matroid.ground_flat
added theorem Matroid.ground_isFlat
deleted theorem Matroid.isClosed_iff_flat
added theorem Matroid.isFlat_closure
deleted theorem Matroid.Base.map
deleted theorem Matroid.Base.mapEmbedding
deleted theorem Matroid.Basis.map
added theorem Matroid.IsBase.map
added theorem Matroid.IsBasis.map
deleted theorem Matroid.comapOn_base_iff
deleted theorem Matroid.comap_base_iff
deleted theorem Matroid.comap_basis'_iff
deleted theorem Matroid.comap_basis_iff
deleted theorem Matroid.mapEquiv_base_iff
deleted theorem Matroid.map_base_iff
deleted theorem Matroid.map_basis_iff'
deleted theorem Matroid.map_basis_iff
added theorem Matroid.map_isBase_iff
modified theorem Matroid.cRank_le_iff
modified theorem Matroid.cRk_le_iff
deleted theorem Matroid.Basis.exchange
deleted theorem Matroid.Basis.transfer
deleted theorem Matroid.Restriction.refl
deleted theorem Matroid.Restriction.trans
deleted def Matroid.Restriction
deleted theorem Matroid.base_restrict_iff