Commit 2025-02-24 08:51 07946e5a

View on Github →

feat(Data/Matroid/Circuit): matroid cocircuits (#21692) We add API for matroid cocircuits, including fundamental cocircuits and their relation to fundamental circuits.

Estimated changes

Modified Mathlib/Data/Matroid/Circuit.lean

added theorem Matroid.Circuit.isCocircuit

added theorem Matroid.Indep.exists_isCocircuit_inter_eq_mem

added theorem Matroid.IsBase.compl_closure_diff_singleton_isCocircuit

added theorem Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuit

added theorem Matroid.IsCircuit.dual_rankPos

added theorem Matroid.IsCircuit.inter_isCocircuit_ne_singleton

added theorem Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter

added theorem Matroid.IsCircuit.isCocircuit_inter_nontrivial

added theorem Matroid.IsCocircuit.circuit

added theorem Matroid.IsCocircuit.subset_ground

added theorem Matroid.coindep_iff_forall_subset_not_isCocircuit

added theorem Matroid.dual_isCocircuit_iff

added theorem Matroid.dual_rankPos_iff_exists_circuit

added theorem Matroid.exists_circuit

added def Matroid.fundCocircuit

added theorem Matroid.fundCocircuit_eq_of_not_mem

added theorem Matroid.fundCocircuit_eq_of_not_mem_ground

added theorem Matroid.fundCocircuit_inter_eq

added theorem Matroid.fundCocircuit_isCocircuit

added theorem Matroid.fundCocircuit_subset_insert_compl

added theorem Matroid.isCocircuit_def

added theorem Matroid.isCocircuit_iff_minimal

added theorem Matroid.isCocircuit_iff_minimal_compl_nonspanning'

added theorem Matroid.isCocircuit_iff_minimal_compl_nonspanning

added theorem Matroid.mem_fundCocircuit

added theorem Matroid.rankPos_iff_exists_isCocircuit

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.IsBase.exchange_base_of_not_mem_closure