English
The exponent of the dihedral group D_n equals lcm(n, 2) (with the n = 0 case giving exponent 0).
Русский
Экспонента диэдральной группы D_n равна \operatorname{lcm}(n,2) (случай n = 0 даёт экспоненту 0).
LaTeX
$$\operatorname{exponent}(\mathrm{DihedralGroup}(n)) = \begin{cases}0, & n = 0 \\ \operatorname{lcm}(n,2), & n > 0.\end{cases}$$
Lean4
theorem exponent : Monoid.exponent (DihedralGroup n) = lcm n 2 :=
by
rcases eq_zero_or_neZero n with (rfl | hn)
· exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one
apply Nat.dvd_antisymm
· apply Monoid.exponent_dvd_of_forall_pow_eq_one
rintro (m | m)
· rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
· rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
exact dvd_lcm_right n 2
· apply lcm_dvd
· convert Monoid.order_dvd_exponent (r (1 : ZMod n))
exact orderOf_r_one.symm
· convert Monoid.order_dvd_exponent (sr (0 : ZMod n))
exact (orderOf_sr 0).symm
