Theorems · Definition · group theory

IsFreeGroupoid.recOn

{G : Type u_1} →
  [inst : CategoryTheory.Groupoid G] →
    {motive : IsFreeGroupoid G → Sort u} →
      (t : IsFreeGroupoid G) →
        ((quiverGenerators : Quiver (IsFreeGroupoid.Generators G)) →
            (of :
                {a b : IsFreeGroupoid.Generators G} →
                  (a ⟶ b) →
                    ((have this := a;
                      this) ⟶
                      b)) →
              (unique_lift :
                  ∀ {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 (of g) = f g) →
                motive { quiverGenerators := quiverGenerators, of := of, unique_lift := unique_lift }) →
          motive t

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

CategoryTheory.Groupoid