Mathlib Map

Theorems · Definition · group theory

DihedralGroup.casesOn

{n : ℕ} →
  {motive : DihedralGroup n → Sort u} →
    (t : DihedralGroup n) →
      ((a : ZMod n) → motive (DihedralGroup.r a)) → ((a : ZMod n) → motive (DihedralGroup.sr a)) → motive t
Defined in
Mathlib.GroupTheory.SpecificGroups.Dihedral
Cited by
2 results in Mathlib
Foundations
Depth 11 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DihedralGroup.ctorIdx · cited by 1DihedralGroup.ctorIdxDihedralGroup.exponent · cited by 1DihedralGroup.exponentDihedralGroup.ctorElim · cited by 0DihedralGroup.ctorElimDihedralGroup.noConfusion · cited by 0DihedralGroup.noConfusionDihedralGroup.noConfusionType · cited by 0DihedralGroup.noConfusion…DihedralGroup.center_eq_bot_of_odd_ne_one · cited by 0DihedralGroup.center_eq_b…ZMod · cited by 1024ZModDihedralGroup · cited by 41DihedralGroupDihedralGroup.casesOnCITED BYCITES

Cites2

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

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

Cited by6

Results whose statement or proof uses this declaration.