English
If 0 < n, then order(a_1) = 2n.
Русский
Если 0 < n, то order(a_1) = 2n.
LaTeX
$$$0 < n \Rightarrow \operatorname{order}(a_1) = 2n$$$
Lean4
/-- If `0 < n`, then `a 1` has order `2 * n`.
-/
@[simp]
theorem orderOf_a_one : orderOf (a 1 : QuaternionGroup n) = 2 * n :=
by
rcases eq_zero_or_neZero n with hn | hn
· subst hn
simp_rw [mul_zero, orderOf_eq_zero_iff']
intro n h
rw [one_def, a_one_pow]
apply mt a.inj
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
simpa using h.ne'
apply (Nat.le_of_dvd (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left
intro h
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
rw [a_one_pow] at h1
injection h1 with h2
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
exact absurd h2.symm (orderOf_pos _).ne
