inv — Mathlib

English

If ζ is a primitive k-th root of unity, then its inverse ζ^{-1} is also a primitive k-th root of unity.

Русский

Если ζ — примитивный корень k-й степени единицы, то его обратный элемент ζ^{-1} также является примитивным корнем той же степени.

LaTeX

$$$IsPrimitiveRoot(\\zeta, k) \\Rightarrow IsPrimitiveRoot(\\zeta^{-1}, k)$$$

Lean4

theorem inv (h : IsPrimitiveRoot ζ k) : IsPrimitiveRoot ζ⁻¹ k :=
  { pow_eq_one := by simp only [h.pow_eq_one, inv_one, inv_pow]
    dvd_of_pow_eq_one := by
      intro l hl
      apply h.dvd_of_pow_eq_one l
      rw [← inv_inj, ← inv_pow, hl, inv_one] }

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