Mathlib Map

Theorems · Definition · group theory

FiniteGrp.of

(G : Type u) → [Group G] → [Finite G] → FiniteGrp.{u}

Construct a term of FiniteGrp from a type endowed with the structure of a finite group.

Defined in
Mathlib.Algebra.Category.Grp.FiniteGrp
Cited by
1 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
GroupFinite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ProfiniteGrp.toFiniteQuotientFunctor · cited by 3ProfiniteGrp.toFiniteQuot…FiniteGaloisIntermediateField.finGaloisGroup · cited by 2FiniteGaloisIntermediateF…FiniteGrp.ofHom · cited by 1FiniteGrp.ofHomProfiniteGrp.ProfiniteCompletion.quotientMap · cited by 1ProfiniteCompletion.quoti…FiniteGrp.ofHom_apply · cited by 0FiniteGrp.ofHom_applyProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram · cited by 0ProfiniteCompletion.finit…Group · cited by 6238GroupFinite · cited by 3029FiniteGrpCat.of · cited by 32GrpCat.ofFiniteGrp · cited by 11FiniteGrpFiniteGrp.ofCITED BYCITES

Cites4

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
  • Finitestatement and proof · cited by 3,029
  • GrpCat.ofproof · cited by 32
  • FiniteGrpstatement · cited by 11

Cited by6

Results whose statement or proof uses this declaration.