Theorems · Definition · group theory

FiniteAddGrp.recOn

{motive : FiniteAddGrp.{u} → Sort u_1} →
  (t : FiniteAddGrp.{u}) →
    ((toAddGrp : AddGrpCat) → [isFinite : Finite ↑toAddGrp] → motive { toAddGrp := toAddGrp, isFinite := isFinite }) →
      motive t

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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

Finitestatement and proof · cited by 3,029
AddGrpCatstatement and proof · cited by 80
AddGrpCat.carrierstatement and proof · cited by 67
FiniteAddGrpstatement and proof · cited by 7

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.