subOneIntegralPowerBasis_gen_prime

English

In a cyclotomic extension with primitive root ζ of order p^(k+1), the generator of the sub-one integral power basis is prime.

Русский

В циклотомическом расширении с примитивным корнем ζ порядка p^(k+1) генератор базиса интегральной мощности представляет собой простое число.

LaTeX

$$$\\text{Prime}\\bigl(h\\zeta.\\text{subOneIntegralPowerBasis}.gen\\bigr)$$$

Lean4

theorem subOneIntegralPowerBasis_gen_prime [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Prime hζ.subOneIntegralPowerBasis.gen := by
  simpa only [subOneIntegralPowerBasis_gen] using hζ.zeta_sub_one_prime

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