isIntegralClosure_adjoin_singleton_of_prime

English

If K is a p-th cyclotomic extension of Q and ζ is a primitive p-th root of unity, then the integral closure of Z in K is the Z-algebra generated by ζ; i.e., 𝒪_K = Z[ζ].

Русский

Если K — p-ое циклотомическое расширение Q и ζ — примитивный p-й корень единицы, то 𝒪_K = Z[ζ].

LaTeX

$$$\operatorname{IsIntegralClosure}(\operatorname{adjoin}_{\mathbb{Z}} (\{\zeta\}\,), \mathbb{Z}, K)$$$

Lean4

theorem isIntegralClosure_adjoin_singleton_of_prime [hcycl : IsCyclotomicExtension { p } ℚ K]
    (hζ : IsPrimitiveRoot ζ p) : IsIntegralClosure (adjoin ℤ ({ ζ } : Set K)) ℤ K :=
  by
  rw [← pow_one p] at hζ hcycl
  exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ

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