English
There is a natural algebra isomorphism between the Z-adjoin of a primitive root ζ and the ring of integers 𝓞K of K, namely adjoin_Z({ζ}) ≃𝖺ℤ 𝓞K.
Русский
Существует естественное алгебраическое изоморфизм между adjoin_Z({ζ}) и 𝓞K: adjoin_Z({ζ}) ≃𝖺ℤ 𝓞K.
LaTeX
$$$\operatorname{adjoin}_{\mathbb{Z}}(\{\zeta\}) \cong_{\mathbb{Z}} \mathcal{O}_K$$$
Lean4
/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p ^ k`-th root of
unity and `K` is a `p ^ k`-th cyclotomic extension of `ℚ`. -/
@[simps!]
noncomputable def _root_.IsPrimitiveRoot.adjoinEquivRingOfIntegers [IsCyclotomicExtension {p ^ k} ℚ K]
(hζ : IsPrimitiveRoot ζ (p ^ k)) : adjoin ℤ ({ ζ } : Set K) ≃ₐ[ℤ] 𝓞 K :=
let _ := isIntegralClosure_adjoin_singleton_of_prime_pow hζ
IsIntegralClosure.equiv ℤ (adjoin ℤ ({ ζ } : Set K)) K (𝓞 K)
