Structures · Combinatorics
Matroid.Finite
Typeclass for a matroid having finite ground set. Just a wrapper for M.E.Finite.
- Defined in
- Mathlib.Combinatorics.Matroid.Basic
- Shape
- One type argument · adds ground_finite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Concrete types that are instances1
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- Matroid.ground_finite
- Matroid.Finite.ground_finite
- Matroid.finite_setOfPred_isRestriction
- Matroid.contract_finite
- Matroid.instFiniteMap
- Matroid.instFiniteMapEmbedding
- Matroid.set_finite
- Matroid.IsRestriction.finite
- Matroid.instFiniteMapEquiv
- Matroid.delete_finite
- Matroid.rankFinite_of_finite
- Matroid.dual_finite
- Matroid.finite_setOf_isRestriction
- Matroid.instFiniteElemERestrictSubtype