Theorems · Theorem · group theory

DihedralGroup.oddCommuteEquiv_symm_apply

∀ {n : ℕ} (hn : Odd n) (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n),
  (DihedralGroup.oddCommuteEquiv hn).symm x =
    match x with
    | Sum.inl i => ⟨(DihedralGroup.sr i, DihedralGroup.r 0), ⋯⟩
    | Sum.inr (Sum.inl j) => ⟨(DihedralGroup.r 0, DihedralGroup.sr j), ⋯⟩
    | Sum.inr (Sum.inr (Sum.inl k)) =>
      ⟨(DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), ⋯⟩
    | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(DihedralGroup.r i, DihedralGroup.r j), ⋯⟩

Defined in

Mathlib.GroupTheory.SpecificGroups.Dihedral

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound