pow_eq_one_iff_dvd — Mathlib

English

For a primitive root ζ of order k, for any l, ζ^l = 1 iff k divides l.

Русский

Для примитивного корня ζ порядка k верно, что ζ^l = 1 тогда и только тогда, когда k делится на л.

LaTeX

$$$IsPrimitiveRoot(\zeta,k) \Rightarrow (\zeta^l = 1 \iff k \mid l)$$$

Lean4

theorem pow_eq_one_iff_dvd (h : IsPrimitiveRoot ζ k) (l : ℕ) : ζ ^ l = 1 ↔ k ∣ l :=
  ⟨h.dvd_of_pow_eq_one l, by rintro ⟨i, rfl⟩; simp only [pow_mul, h.pow_eq_one, one_pow]⟩

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