English
Under suitable hypotheses, CyclotomicRing n A K embeds into its field of fractions CyclotomicField n K, i.e. there is a fraction-field isomorphism structure making CyclotomicRing a subring of CyclotomicField.
Русский
При надлежащих условиях CyclotomicRing n A K embeds в своё поле дробей CyclotomicField n K; существует частично изоморфизм дробей, делающий CyclotomicRing подкольцом CyclotomicField.
LaTeX
$$$\\text{IsFractionRing}(\\operatorname{CyclotomicRing}(n,A,K),\\operatorname{CyclotomicField}(n,K))$$$
Lean4
theorem eq_adjoin_primitive_root {μ : CyclotomicField n K} (h : IsPrimitiveRoot μ n) :
CyclotomicRing n A K = adjoin A ({ μ } : Set (CyclotomicField n K)) :=
by
rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]
simp [CyclotomicRing, NeZero.ne n]
