cyclotomicRing_isIntegralClosure_of_prime

English

For a prime p, the integral closure inside the p-th cyclotomic field is the cyclotomic ring over Z, i.e., 𝒪_{K} = CyclotomicRing(p) over Z in the p-th cyclotomic field.

Русский

Для простого p целочисленное замыкание внутри p-й циклотомической области равно кольцу циклотомии над Z в p-й циклотомической области.

LaTeX

$$$\operatorname{IsIntegralClosure}(\operatorname{CyclotomicRing}(p)\, \mathbb{Z}, \mathbb{Z}, \operatorname{CyclotomicField}(p))$$$

Lean4

theorem cyclotomicRing_isIntegralClosure_of_prime : IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ) :=
  by
  rw [← pow_one p]
  exact cyclotomicRing_isIntegralClosure_of_prime_pow

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