Mathlib Map

Theorems · Theorem · group theory

IsKleinFour.card_four

∀ {G : Type u_1} {inst : Group G} [self : IsKleinFour G], Nat.card G = 4
Defined in
Mathlib.GroupTheory.SpecificGroups.KleinFour
Cited by
2 results in Mathlib
Foundations
Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
IsKleinFour
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsKleinFour.card_four' · cited by 2IsKleinFour.card_four'IsKleinFour.not_isCyclic · cited by 0IsKleinFour.not_isCyclicGroup · cited by 6238GroupNat.card · cited by 844Nat.cardIsKleinFour · cited by 11IsKleinFourIsKleinFour.card_fourCITED BYCITES

Cites3

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
  • Nat.cardstatement · cited by 844
  • IsKleinFourstatement and proof · cited by 11

Cited by2

Results whose statement or proof uses this declaration.