Theorems · Theorem · group theory

IsFreeGroupoid.unique_lift

∀ {G : Type u_1} {inst : CategoryTheory.Groupoid G} [self : IsFreeGroupoid G] {X : Type v} [inst_1 : Group X]
  (f : Quiver.Labelling (IsFreeGroupoid.Generators G) X),
  ∃! F, ∀ (a b : IsFreeGroupoid.Generators G) (g : a ⟶ b), F.map (IsFreeGroupoid.of g) = f g

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

2 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

IsFreeGroupoidGroup