zpow_eq_one_iff_dvd — Mathlib

English

If h states that ζ is a primitive root of order k, then for any integer l we have ζ^l = 1 iff k divides l.

Русский

Если ζ является примитивным корнем порядка k, тогда для любого целого l выполняется ζ^l = 1 тогда и только тогда, когда k делится на l.

LaTeX

$$$IsPrimitiveRoot(\\zeta, k) \\Rightarrow ∀ l : \\mathbb{Z}, \\ \\zeta^l = 1 \\iff (k : \\mathbb{Z}) \\mid l$$$

Lean4

theorem zpow_eq_one_iff_dvd (h : IsPrimitiveRoot ζ k) (l : ℤ) : ζ ^ l = 1 ↔ (k : ℤ) ∣ l :=
  by
  by_cases h0 : 0 ≤ l
  · lift l to ℕ using h0; exact_mod_cast h.pow_eq_one_iff_dvd l
  · have : 0 ≤ -l := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
    lift -l to ℕ using this with l' hl'
    rw [← dvd_neg, ← hl']
    norm_cast
    rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]

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