Mathlib Map

Theorems · Theorem · group theory

DihedralGroup.card

∀ {n : ℕ} [inst : NeZero n], Fintype.card (DihedralGroup n) = 2 * n

If 0 < n, then DihedralGroup n has 2n elements.

Defined in
Mathlib.GroupTheory.SpecificGroups.Dihedral
Cited by
2 results in Mathlib
Foundations
Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NeZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DihedralGroup.nat_card · cited by 3DihedralGroup.nat_cardDihedralGroup.not_isCyclic · cited by 1DihedralGroup.not_isCyclicEquiv.symm · cited by 3681Equiv.symmFintype.card · cited by 1386Fintype.cardtwo_mul · cited by 232two_mulDihedralGroup · cited by 41DihedralGroupZMod.card · cited by 36ZMod.cardFintype.card_eq · cited by 19Fintype.card_eqFintype.card_sum · cited by 12Fintype.card_sumDihedralGroup.equivSum · cited by 3DihedralGroup.equivSumDihedralGroup.cardCITED BYCITES

Cites8

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

Cited by2

Results whose statement or proof uses this declaration.