Mathlib Map

Theorems · Definition · group theory

Group.FG.casesOn

{G : Type u_3} →
  [inst : Group G] → {motive : Group.FG G → Sort u} → (t : Group.FG G) → ((out : ⊤.FG) → motive ⋯) → motive t
Defined in
Mathlib.GroupTheory.Finiteness
Cited by
1 results in Mathlib
Foundations
Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Group.fg_iff_nonempty_finite_generators · cited by 0Group.fg_iff_nonempty_fin…Top.top · cited by 9680Top.topGroup · cited by 6238GroupSubgroup · cited by 3593SubgroupGroup.FG · cited by 40Group.FGSubgroup.FG · cited by 18Subgroup.FGFG.casesOnCITED BYCITES

Cites5

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

  • Top.topstatement and proof · cited by 9,680
  • Groupstatement and proof · cited by 6,238
  • Subgroupstatement · cited by 3,593
  • Group.FGstatement and proof · cited by 40
  • Subgroup.FGstatement and proof · cited by 18

Cited by1

Results whose statement or proof uses this declaration.