Mathlib Map

Theorems · Theorem · group theory

IsFreeGroupoid.SpanningTree.treeHom_root

∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)],
  IsFreeGroupoid.SpanningTree.treeHom T (IsFreeGroupoid.SpanningTree.root'✝ T) =
    CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
Defined in
Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Cited by
1 results in Mathlib
Foundations
Depth 16 from the axioms · uses Classical.choice
Assumes
CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsFreeGroupoid.SpanningTree.endIsFree · cited by 0SpanningTree.endIsFreeQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.Groupoid · cited by 182CategoryTheory.Groupoidtrans · cited by 111transQuiver.Symmetrify · cited by 28Quiver.SymmetrifyIsFreeGroupoid.Generators · cited by 11IsFreeGroupoid.GeneratorsIsFreeGroupoid · cited by 11IsFreeGroupoidQuiver.Arborescence · cited by 7Quiver.ArborescenceWideSubquiver.toType · cited by 7WideSubquiver.toTypeWideSubquiver · cited by 7WideSubquiverIsFreeGroupoid.SpanningTree.treeHom · cited by 4SpanningTree.treeHomIsFreeGroupoid.SpanningTree.treeHom_eq · cited by 2SpanningTree.treeHom_eqSpanningTree.treeHom_rootCITED BYCITES

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.