orderOf_one_add_four_mul — Mathlib

English

For odd a, the order of 1 + 4a in ZMod(2^{n+2}) is 2^n.

Русский

При нечетном a порядок 1 + 4a в ZMod(2^{n+2}) равен 2^n.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{Z}, \\\\text{Odd}(a) \\\\Rightarrow \\\\operatorname{orderOf} (1 + 4 a \\\\bmod 2^{n+2}) = 2^{n}. $$$$

Lean4

theorem orderOf_one_add_four_mul (a : ℤ) (ha : Odd a) (n : ℕ) : orderOf (1 + 4 * a : ZMod (2 ^ (n + 2))) = 2 ^ n :=
  by
  convert orderOf_one_add_mul_prime_pow Nat.prime_two 2 two_ne_zero le_rfl a ?_ n using 1
  · norm_num
  · rwa [← Int.not_even_iff_odd, even_iff_two_dvd] at ha

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