order_ω — Mathlib

English

The multiplicative order of ωUnit(p+2) equals 2^{p+2}.

Русский

Порядок элемента ωUnit(p+2) в группе единиц равен 2^{p+2}.

LaTeX

$$$\operatorname{orderOf}(\omegaUnit(p+2)) = 2^{p+2}$$$

Lean4

/-- The order of `ω` in the unit group is exactly `2^p`. -/
theorem order_ω (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : orderOf (ωUnit (p' + 2)) = 2 ^ (p' + 2) :=
  by
  apply Nat.eq_prime_pow_of_dvd_least_prime_pow
  · exact Nat.prime_two
  · intro o
    have ω_pow :=
      congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) <|
        orderOf_dvd_iff_pow_eq_one.1 o
    have h : (1 : ZMod (q (p' + 2))) = -1 := congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
    haveI : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
    apply ZMod.neg_one_ne_one h.symm
  · apply orderOf_dvd_iff_pow_eq_one.2
    apply Units.ext
    push_cast
    exact ω_pow_eq_one p' h

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