orderOf_xa — Mathlib

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

Похожие утверждения