English
For all i, orderOf(xa_i) = 4.
Русский
Для любого i: orderOf(xa_i) = 4.
LaTeX
$$$\operatorname{orderOf}(xa_i) = 4$$$
Lean4
/-- If `0 < n`, then `xa i` has order 4.
-/
@[simp]
theorem orderOf_xa [NeZero n] (i : ZMod (2 * n)) : orderOf (xa i) = 4 :=
by
change _ = 2 ^ 2
haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
apply orderOf_eq_prime_pow
· intro h
simp only [pow_one, xa_sq] at h
injection h with h'
apply_fun ZMod.val at h'
apply_fun (· / n) at h'
simp only [ZMod.val_natCast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self, Nat.div_self (NeZero.pos n),
reduceCtorEq] at h'
· simp