Mathlib Map

Theorems · Inductive type · group theory

FiniteAddGrp

Type (u + 1)

The category of finite additive groups.

Defined in
Mathlib.Algebra.Category.Grp.FiniteGrp
Cited by
7 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ProfiniteAddGrp.diagram · cited by 6ProfiniteAddGrp.diagramFiniteAddGrp.toAddGrp · cited by 4FiniteAddGrp.toAddGrpProfiniteAddGrp.toFiniteQuotientFunctor · cited by 2ProfiniteAddGrp.toFiniteQ…FiniteAddGrp.ofHom · cited by 1FiniteAddGrp.ofHomFiniteAddGrp.mk.inj · cited by 1mk.injFiniteAddGrp.mk.noConfusion · cited by 1mk.noConfusionProfiniteAddGrp.ProfiniteCompletion.diagram · cited by 1ProfiniteCompletion.diagr…FiniteAddGrp.of · cited by 1FiniteAddGrp.ofFiniteAddGrp.ofHom_apply · cited by 0FiniteAddGrp.ofHom_applyFiniteAddGrp.recOn · cited by 0FiniteAddGrp.recOnProfiniteAddGrp.diagram_map · cited by 0ProfiniteAddGrp.diagram_m…ProfiniteAddGrp.diagram_obj · cited by 0ProfiniteAddGrp.diagram_o…FiniteAddGrp.mk.injEq · cited by 0mk.injEqFiniteAddGrp.mk.sizeOf_spec · cited by 0mk.sizeOf_specProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram · cited by 0ProfiniteCompletion.finit…FiniteAddGrpCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by23

Results whose statement or proof uses this declaration.