Theorems · Definition · combinatorics
SimpleGraph.IsRegularOfDegree
{V : Type u_1} → (G : SimpleGraph V) → [G.LocallyFinite] → ℕ → PropA locally finite simple graph is regular of degree d if every vertex has degree d.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Finite
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Quot.sound
- Assumes
- SimpleGraph.LocallyFinite
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.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.degreeproof · cited by 112
- SimpleGraph.LocallyFinitestatement and proof · cited by 18
Cited by12
Results whose statement or proof uses this declaration.
- SimpleGraph.IsSRGWith.regularstatement · cited by 4
- SimpleGraph.IsRegularOfDegree.degree_eqstatement and proof · cited by 3
- SimpleGraph.IsRegularOfDegree.topstatement · cited by 3
- SimpleGraph.IsRegularOfDegree.botstatement · cited by 1
- SimpleGraph.IsRegularOfDegree.complstatement and proof · cited by 1
- SimpleGraph.IsRegularOfDegree.maxDegree_eqstatement and proof · cited by 1
- SimpleGraph.IsRegularOfDegree.minDegree_eqstatement and proof · cited by 1
- SimpleGraph.IsSRGWith.compl_is_regularstatement and proof · cited by 1
- SimpleGraph.adjMatrix_mulVec_const_apply_of_regularstatement and proof · cited by 0
- SimpleGraph.IsRegularOfDegree.of_isEmptystatement · cited by 0
- SimpleGraph.IsSRGWith.casesOnstatement and proof · cited by 0
- SimpleGraph.IsSRGWith.recOnstatement and proof · cited by 0