Commit 2025-03-25 13:39 69f9139b

View on Github →

feat(Data/Matroid): matroid deletion/contraction (#23276) We define deletions and contractions of sets in matroids. We provide basic API for deletion, and its interaction with most of the existing matroid notions in mathlib. The API for contraction is more complicated, so to limit size of this first PR, we just give the definition and the fact that it is dual to deletion.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matroid/Minor/Basic.lean

added theorem Matroid.Coindep.delete_isBase_iff

added theorem Matroid.Coindep.delete_rankPos

added theorem Matroid.Coindep.delete_spanning_iff

added theorem Matroid.Indep.indep_delete_of_disjoint

added theorem Matroid.Indep.of_delete

added theorem Matroid.IsBasis.delete

added theorem Matroid.IsBasis.of_delete

added theorem Matroid.IsCircuit.of_delete

added theorem Matroid.IsNonloop.of_delete

added theorem Matroid.IsRestriction.exists_eq_delete

added theorem Matroid.IsRestriction.isRestriction_deleteElem

added theorem Matroid.IsRestriction.restrict_delete_of_disjoint

added theorem Matroid.circuit_iff_delete_of_disjoint

added def Matroid.contract

added theorem Matroid.contract_comm

added theorem Matroid.contract_contract

added def Matroid.delete

added theorem Matroid.deleteElem_eq_self

added theorem Matroid.deleteElem_indep_iff

added theorem Matroid.delete_closure_eq

added theorem Matroid.delete_comm

added theorem Matroid.delete_compl

added theorem Matroid.delete_delete

added theorem Matroid.delete_delete_eq_delete_diff

added theorem Matroid.delete_dep_iff

added theorem Matroid.delete_empty

added theorem Matroid.delete_eq_delete_iff

added theorem Matroid.delete_eq_restrict

added theorem Matroid.delete_eq_self_iff

added theorem Matroid.delete_ground

added theorem Matroid.delete_indep_iff

added theorem Matroid.delete_inter_ground_eq

added theorem Matroid.delete_isBase_iff

added theorem Matroid.delete_isBasis'_iff

added theorem Matroid.delete_isBasis_iff

added theorem Matroid.delete_isCircuit_iff

added theorem Matroid.delete_isLoop_iff

added theorem Matroid.delete_isNonloop_iff

added theorem Matroid.delete_isRestriction

added theorem Matroid.delete_loops_eq

added theorem Matroid.delete_subset_ground

added theorem Matroid.dual_contract

added theorem Matroid.dual_contract_delete

added theorem Matroid.dual_contract_dual

added theorem Matroid.dual_delete

added theorem Matroid.dual_delete_contract

added theorem Matroid.dual_delete_dual

added theorem Matroid.indep_iff_delete_of_disjoint

added theorem Matroid.isNonloop_iff_delete_of_not_mem

added theorem Matroid.isRestriction_iff_exists_eq_delete

added theorem Matroid.restrict_compl