Theorems · Inductive type · combinatorics

Quiver.SchreierGraph

(V : Type u_1) → {M : Type u_2} → [SMul M V] → {S : Type u_3} → (S → M) → Type u_1

A Schreier graph for a monoid M acting on V with generators ι : S → M. Vertices are elements of V, and there is an edge from x to y for each s : S such that ι s • x = y.

Defined in

Mathlib.Combinatorics.Quiver.Schreier

Cited by

17 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

SMul