Mathlib Map

Theorems · Definition · category theory

GrpCat.of

(M : Type u) → [Group M] → GrpCat

Construct a bundled GrpCat from the underlying type and typeclass.

Defined in
Mathlib.Algebra.Category.Grp.Basic
Cited by
32 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

GrpCat.ofHom · cited by 23GrpCat.ofHomCategoryTheory.yonedaGrpObj · cited by 9CategoryTheory.yonedaGrpO…GrpCat.shrinkFunctor · cited by 6GrpCat.shrinkFunctorCategoryTheory.PreGaloisCategory.autGaloisSystem · cited by 6PreGaloisCategory.autGalo…ProfiniteGrp.ProfiniteCompletion.eta · cited by 6ProfiniteCompletion.etaAddGrpCat.toGrp · cited by 4AddGrpCat.toGrpMonCat.units · cited by 3MonCat.unitsProfiniteGrp.ProfiniteCompletion.lift · cited by 3ProfiniteCompletion.liftGrpCat.uliftFunctor · cited by 2GrpCat.uliftFunctorProfiniteGrp.ProfiniteCompletion.preimage · cited by 2ProfiniteCompletion.preim…FiniteGrp.of · cited by 1FiniteGrp.ofGrpCat.subsingleton_of_isZero · cited by 1GrpCat.subsingleton_of_is…CategoryTheory.PreGaloisCategory.autGaloisSystem_map · cited by 1PreGaloisCategory.autGalo…GrpCat.SurjectiveOfEpiAuxs.comp_eq · cited by 1SurjectiveOfEpiAuxs.comp_…ProfiniteGrp.ProfiniteCompletion.lift_eta · cited by 1ProfiniteCompletion.lift_…Group · cited by 6238GroupGrpCat · cited by 146GrpCatGrpCat.ofCITED BYCITES

Cites2

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

  • Groupstatement and proof · cited by 6,238
  • GrpCatstatement · cited by 146

Cited by51

Results whose statement or proof uses this declaration.