Commit 2025-03-31 15:04 8eb2ac74

View on Github →

feat(Data/Matroid/Loop): matroid coloops (#23373) We give API for the dual notion Matroid.IsColoop of Matroid.IsLoop.

Estimated changes

Modified Mathlib/Data/Matroid/Loop.lean

added theorem Matroid.IsBase.coloops_subset

added theorem Matroid.IsBase.isColoop_iff_forall_not_mem_fundCircuit

added theorem Matroid.IsBase.mem_of_isColoop

added theorem Matroid.IsBasis'.inter_coloops_subset

added theorem Matroid.IsBasis.inter_coloops_subset

added theorem Matroid.IsCircuit.disjoint_coloops

added theorem Matroid.IsCircuit.not_isColoop_of_mem

added theorem Matroid.IsColoop.dual_isLoop

added theorem Matroid.IsColoop.insert_indep_of_indep

added theorem Matroid.IsColoop.isCocircuit

added theorem Matroid.IsColoop.isNonloop

added theorem Matroid.IsColoop.mem_closure_iff_mem

added theorem Matroid.IsColoop.mem_ground

added theorem Matroid.IsColoop.mem_of_isBase

added theorem Matroid.IsColoop.mem_of_mem_closure

added theorem Matroid.IsColoop.not_mem_closure_of_not_mem

added theorem Matroid.IsColoop.not_mem_isCircuit

added def Matroid.IsColoop

added theorem Matroid.IsLoop.dual_isColoop

added theorem Matroid.IsLoop.not_isColoop

added theorem Matroid.closure_diff_eq_of_subset_coloops

added theorem Matroid.closure_disjoint_coloops_of_disjoint_coloops

added theorem Matroid.closure_disjoint_of_disjoint_of_subset_coloops

added theorem Matroid.closure_eq_of_subset_coloops

added theorem Matroid.closure_insert_isColoop_eq

added theorem Matroid.closure_inter_coloops_eq

added theorem Matroid.closure_inter_eq_of_subset_coloops

added theorem Matroid.closure_union_coloops_eq

added theorem Matroid.closure_union_eq_of_subset_coloops

added def Matroid.coloops

added theorem Matroid.coloops_indep

added theorem Matroid.coloops_subset_ground

modified theorem Matroid.comap_isNonloop_iff

added theorem Matroid.diff_coloops_indep_iff

added theorem Matroid.diff_indep_iff_indep_of_subset_coloops

added theorem Matroid.dual_coloops

added theorem Matroid.dual_isColoop_iff_isLoop

added theorem Matroid.dual_isLoop_iff_isColoop

added theorem Matroid.dual_loops

added theorem Matroid.exists_mem_isCircuit_of_not_isColoop

added theorem Matroid.ext_indep_disjoint_loops_coloops

modified theorem Matroid.freeOn_isNonloop_iff

modified theorem Matroid.indep_singleton

added theorem Matroid.isColoop_iff_diff_closure

added theorem Matroid.isColoop_iff_diff_not_spanning

added theorem Matroid.isColoop_iff_forall_mem_closure_iff_mem'

added theorem Matroid.isColoop_iff_forall_mem_closure_iff_mem

added theorem Matroid.isColoop_iff_forall_mem_compl_isCircuit

added theorem Matroid.isColoop_iff_forall_mem_isBase

added theorem Matroid.isColoop_iff_forall_not_mem_isCircuit

added theorem Matroid.isColoop_iff_mem_loops

added theorem Matroid.isColoop_iff_not_mem_closure_compl

added theorem Matroid.isColoop_tfae

modified theorem Matroid.not_isLoop_iff

modified theorem Matroid.not_isNonloop_iff

modified theorem Matroid.restrict_isNonloop_iff

added theorem Matroid.singleton_isCocircuit

added theorem Matroid.union_coloops_indep_iff

added theorem Matroid.union_indep_iff_indep_of_subset_coloops

modified theorem Matroid.uniqueBaseOn_isNonloop_iff