Commit 2025-04-03 15:46 89fd4fe6

View on Github →

feat(Data/Matroid/Minor): organize minor API (#23591) This gives some API for the interaction of Matroid.contract with independence and bases, and tidies up Matroid.Minor.Basic by introducing section headings. Split from #23557 .

Estimated changes

Modified Mathlib/Data/Matroid/Loop.lean

added theorem Matroid.restrict_isColoop_iff

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

added theorem Matroid.Coindep.coindep_contract_of_disjoint

added theorem Matroid.Dep.of_contract

added theorem Matroid.Indep.contract_dep_iff

added theorem Matroid.Indep.contract_indep_iff

added theorem Matroid.Indep.contract_isBase_iff

added theorem Matroid.Indep.diff_indep_contract_of_subset

added theorem Matroid.Indep.of_contract

added theorem Matroid.Indep.union_indep_iff_contract_indep

added theorem Matroid.Indep.union_isBasis_union_of_contract_isBasis

added theorem Matroid.IsBasis'.contract_dep_iff

added theorem Matroid.IsBasis'.contract_eq_contract_delete

added theorem Matroid.IsBasis'.contract_indep_diff_iff

added theorem Matroid.IsBasis'.contract_indep_iff

added theorem Matroid.IsBasis'.contract_isBasis'

added theorem Matroid.IsBasis'.contract_isBasis'_diff_diff_of_subset

added theorem Matroid.IsBasis'.contract_isBasis'_diff_of_subset

added theorem Matroid.IsBasis'.contract_isBasis_of_indep

added theorem Matroid.IsBasis'.contract_isBasis_union_union

added theorem Matroid.IsBasis.contract_dep_iff

added theorem Matroid.IsBasis.contract_diff_isBasis_diff

added theorem Matroid.IsBasis.contract_eq_contract_delete

added theorem Matroid.IsBasis.contract_indep_diff_iff

added theorem Matroid.IsBasis.contract_indep_iff

added theorem Matroid.IsBasis.contract_indep_iff_of_disjoint

added theorem Matroid.IsBasis.contract_isBasis

added theorem Matroid.IsBasis.contract_isBasis_diff_diff_of_subset

added theorem Matroid.IsBasis.contract_isBasis_of_disjoint

added theorem Matroid.IsBasis.contract_isBasis_of_disjoint_indep

added theorem Matroid.IsBasis.contract_isBasis_of_indep

added theorem Matroid.IsBasis.contract_isBasis_of_isBasis'

added theorem Matroid.IsBasis.contract_isBasis_union_union

added theorem Matroid.IsNonloop.contractElem_indep_iff

added theorem Matroid.coindep_contract_iff

added theorem Matroid.contractElem_eq_self

added theorem Matroid.contract_contract_eq_contract_diff

added theorem Matroid.contract_empty

added theorem Matroid.contract_eq_contract_iff

added theorem Matroid.contract_eq_self_iff

added theorem Matroid.contract_ground

added theorem Matroid.contract_ground_subset_ground

added theorem Matroid.contract_inter_ground_eq

added theorem Matroid.contract_isCocircuit_iff

added theorem Matroid.delete_closure_eq_of_disjoint

added theorem Matroid.delete_isColoop_iff

Modified scripts/noshake.json