Commit 2025-04-08 16:19 49351b9f

View on Github →

feat(Data/Matroid/Minor): contraction API (#23557) We give API for the interaction of matroid contraction with circuits, loops/coloops, closure and finiteness.

Estimated changes

Modified Mathlib/Data/Matroid/Loop.lean

added theorem Matroid.eq_loopyOn_iff_loops_eq

added theorem Matroid.isColoop_iff_mem_coloops

deleted theorem Matroid.isColoop_iff_mem_loops

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

added theorem Matroid.IsBasis.diff_subset_loops_contract

added theorem Matroid.IsCircuit.contractElem_isCircuit

added theorem Matroid.IsCircuit.contract_dep

added theorem Matroid.IsCircuit.contract_dep_of_not_subset

added theorem Matroid.IsCircuit.contract_diff_isCircuit

added theorem Matroid.IsCircuit.contract_isCircuit

added theorem Matroid.IsCircuit.exists_subset_isCircuit_of_contract

added theorem Matroid.IsCocircuit.delete_diff_isCocircuit

added theorem Matroid.IsCocircuit.delete_isCocircuit

added theorem Matroid.IsCocircuit.of_contract

added theorem Matroid.IsNonloop.of_contract

added theorem Matroid.Spanning.contract

added theorem Matroid.Spanning.contract_eq_loopyOn

added theorem Matroid.contract_closure_eq

added theorem Matroid.contract_closure_eq_contract_delete

added theorem Matroid.contract_coloops_eq

added theorem Matroid.contract_eq_delete_of_subset_coloops

added theorem Matroid.contract_eq_delete_of_subset_loops

added theorem Matroid.contract_isColoop_iff

added theorem Matroid.contract_isLoop_iff_mem_closure

added theorem Matroid.contract_isNonloop_iff

added theorem Matroid.contract_loops_eq

added theorem Matroid.contract_spanning_iff'

added theorem Matroid.contract_spanning_iff