Theorems · Theorem · combinatorics

Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_fst

∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (x_1 : Quiver.Costar (Quiver.SingleObj.star S)),
  ((Quiver.SchreierGraph.labellingCostarEquiv ι x).symm x_1).fst = (ι x_1.snd)⁻¹ • x

Defined in

Mathlib.Combinatorics.Quiver.Schreier

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

GroupMulAction