Theorems · Definition · group theory
FiniteAddGrp.noConfusion
{P : Sort u_1} → {t t' : FiniteAddGrp.{u}} → t = t' → FiniteAddGrp.noConfusionType P t t'- Defined in
- Mathlib.Algebra.Category.Grp.FiniteGrp
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finiteproof · cited by 3,029
- AddGrpCatproof · cited by 80
- AddGrpCat.carrierproof · cited by 67
- FiniteAddGrpstatement and proof · cited by 7
- FiniteAddGrp.casesOnproof · cited by 0
- FiniteAddGrp.noConfusionTypestatement · cited by 0
Cited by1
Results whose statement or proof uses this declaration.
- FiniteAddGrp.mk.noConfusionproof · cited by 1