pow_ne_one_of_pos_of_lt — Mathlib

English

If h is primitive root, and l ≠ 0 with l < k, then ζ^l ≠ 1.

Русский

Если ζ примитивного корня порядка k, и l ≠ 0 и l < k, то ζ^l ≠ 1.

LaTeX

$$$IsPrimitiveRoot(\zeta,k) \land l \neq 0 \land l < k \Rightarrow (\zeta^l \neq 1)$$$

Lean4

theorem pow_ne_one_of_pos_of_lt (h : IsPrimitiveRoot ζ k) (h0 : l ≠ 0) (hl : l < k) : ζ ^ l ≠ 1 :=
  mt (Nat.le_of_dvd (Nat.pos_iff_ne_zero.mpr h0) ∘ h.dvd_of_pow_eq_one _) <| not_le_of_gt hl

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