ring_of_integers' — Mathlib

English

If hζ is a primitive root of order k, then hζ.toInteger is again a primitive root of order k.

Русский

Если hζ — примитивный корень порядка k, то hζ.toInteger снова примитивный корень порядка k.

LaTeX

$$$$ \text{IsPrimitiveRoot}(h\zeta^{\mathrm{toInteger}}, k) $$$$

Lean4

/-- The ring of integers of a `p`-th cyclotomic extension of `ℚ` is a cyclotomic extension. -/
instance _root_.IsCyclotomicExtension.ring_of_integers' [IsCyclotomicExtension { p } ℚ K] :
    IsCyclotomicExtension { p } ℤ (𝓞 K) :=
  let _ := (zeta_spec p ℚ K).adjoin_isCyclotomicExtension ℤ
  IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec p ℚ K).adjoinEquivRingOfIntegers'

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