Mathlib Map

Theorems · Definition · group theory

DihedralGroup.equivSum

{n : ℕ} → DihedralGroup n ≃ ZMod n ⊕ ZMod n

The equivalence between the dihedral group and the sum of ZMods.

Defined in
Mathlib.GroupTheory.SpecificGroups.Dihedral
Cited by
3 results in Mathlib
Foundations
Depth 14 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DihedralGroup.card · cited by 2DihedralGroup.cardDihedralGroup.equivSum_apply · cited by 0DihedralGroup.equivSum_ap…DihedralGroup.equivSum_symm_apply · cited by 0DihedralGroup.equivSum_sy…Equiv · cited by 8337EquivZMod · cited by 1024ZModDihedralGroup · cited by 41DihedralGroupDihedralGroup.equivSumCITED BYCITES

Cites3

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

  • Equivstatement · cited by 8,337
  • ZModstatement and proof · cited by 1,024
  • DihedralGroupstatement and proof · cited by 41

Cited by3

Results whose statement or proof uses this declaration.