unique

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

English

If two primitive roots ζ give IsPrimitiveRoot of orders k and l respectively, then k = l.

Русский

Если одно и то же ζ задаёт два примитивных порядка k и l, то k = l.

LaTeX

$$$$\text{If } IsPrimitiveRoot(\zeta,k) \text{ and } IsPrimitiveRoot(\zeta,l) \text{ then } k = l.$$$$

Lean4

theorem unique {ζ : M} (hk : IsPrimitiveRoot ζ k) (hl : IsPrimitiveRoot ζ l) : k = l :=
  Nat.dvd_antisymm (hk.2 _ hl.1) (hl.2 _ hk.1)

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

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

Разделы

Аффилиация

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