Structures · Combinatorics
Matroid.Loopless
A Matroid is Loopless if it has no loop
- Defined in
- Mathlib.Combinatorics.Matroid.Loop
- Shape
- One type argument · adds loops_eq_empty
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- Matroid.isNonloop_of_loopless
- Matroid.removeLoops_eq_self
- Matroid.loops_eq_empty
- Matroid.Loopless.loops_eq_empty
- Matroid.IsRestriction.isRestriction_removeLoops
- Matroid.Loopless.ground_eq
- Matroid.not_isLoop
- Matroid.IsRestriction.loopless
- Matroid.subsingleton_indep
- Matroid.instRankPosOfNonemptyOfLoopless
- Matroid.eRk_singleton_eq
Ancestors0
No ancestors.