English
The exponent of QuaternionGroup n equals 2 * lcm(n, 2).
Русский
Порядок группы QuaternionGroup n равен 2 * НСК (n, 2).
LaTeX
$$$\mathrm{exponent}(\text{QuaternionGroup}(n)) = 2 \cdot \operatorname{lcm}(n,2)$$$
Lean4
theorem exponent : Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2 :=
by
rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]
norm_num
rcases eq_zero_or_neZero n with hn | hn
· subst hn
simp only [lcm_zero_left, mul_zero]
exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_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_a]
refine Nat.dvd_trans ⟨gcd (2 * n) m.val, ?_⟩ (dvd_lcm_left (2 * n) 4)
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm
· rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]
exact dvd_lcm_right (2 * n) 4
· apply lcm_dvd
· convert Monoid.order_dvd_exponent (a 1)
exact orderOf_a_one.symm
· convert Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))
exact (orderOf_xa 0).symm
