English
In DihedralGroup n, for i ∈ ZMod n and k ∈ Z, (r i)^{k} = r (i k).
Русский
В DihedralGroup n для i ∈ ZMod n и k ∈ Z выполняется (r i)^{k} = r (i k).
LaTeX
$$$(r i)^{k} = r(i k) \quad (i \in ZMod\ n, k \in Z)$$$
Lean4
/-- The group structure on `DihedralGroup n`.
-/
instance : Group (DihedralGroup n) where
mul := mul
mul_assoc := by rintro (a | a) (b | b) (c | c) <;> simp only [(· * ·), mul] <;> ring_nf
one := one
one_mul := by
rintro (a | a)
· exact congr_arg r (zero_add a)
· exact congr_arg sr (sub_zero a)
mul_one := by
rintro (a | a)
· exact congr_arg r (add_zero a)
· exact congr_arg sr (add_zero a)
inv := inv
inv_mul_cancel := by
rintro (a | a)
· exact congr_arg r (neg_add_cancel a)
· exact congr_arg r (sub_self a)
