Theorems · Definition · combinatorics
Matroid.IsColoop
{α : Type u_1} → Matroid α → α → PropA coloop is a loop of the dual matroid.
See Matroid.isColoop_tfae for a number of equivalent definitions.
- Defined in
- Mathlib.Combinatorics.Matroid.Loop
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matroidstatement and proof · cited by 1,258
- Matroid.dualproof · cited by 79
- Matroid.IsLoopproof · cited by 55
Cited by38
Results whose statement or proof uses this declaration.
- Matroid.IsColoop.mem_groundstatement and proof · cited by 6
- Matroid.IsColoop.mem_closure_iff_memstatement and proof · cited by 5
- Matroid.isColoop_tfaestatement and proof · cited by 4
- Matroid.IsColoop.notMem_isCircuitstatement and proof · cited by 3
- Matroid.isColoop_iff_forall_mem_isBasestatement and proof · cited by 3
- Matroid.isColoop_iff_sdiff_not_spanningstatement and proof · cited by 3
- Matroid.IsColoop.dual_isLoopstatement and proof · cited by 2
- Matroid.IsColoop.mem_of_isBasestatement and proof · cited by 2
- Matroid.IsLoop.dual_isColoopstatement · cited by 2
- Matroid.dual_isLoop_iff_isColoopstatement and proof · cited by 2
- Matroid.isColoop_iff_forall_mem_closure_iff_memstatement and proof · cited by 2
- Matroid.isColoop_iff_sdiff_closurestatement · cited by 2