isUnit — Mathlib

English

If h is a primitive root of order k with k ≠ 0, then ζ is a unit.

Русский

Если h является примитивным корнем порядка k с k ≠ 0, то ζ является единицей

LaTeX

$$$IsPrimitiveRoot(\zeta,k) \land k \neq 0 \Rightarrow IsUnit(\zeta)$$$

Lean4

theorem isUnit (h : IsPrimitiveRoot ζ k) (h0 : k ≠ 0) : IsUnit ζ :=
  by
  apply isUnit_of_mul_eq_one ζ (ζ ^ (k - 1))
  rw [← pow_succ', Nat.sub_one_add_one h0, h.pow_eq_one]

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