inv_iff

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

URI: https://scilib.ai/kg/mathlib#IsPrimitiveRoot.inv_iff

English

ζ⁻¹ is primitive of order k iff ζ is primitive of order k.

Русский

ζ⁻¹ имеет порядок k тогда же, когда ζ имеет порядок k.

LaTeX

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

Lean4

@[simp]
theorem inv_iff : IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k :=
  ⟨fun h ↦ inv_inv ζ ▸ inv h, fun h ↦ inv h⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru