English
Let A and K be appropriate rings and let CyclotomicRing n A K embed into CyclotomicField n K via the algebra map. Then this embedding is injective: distinct elements of the cyclotomic ring have distinct images in the cyclotomic field.
Русский
Пусть A и K — подходящие кольца и через алгебраическое отображениеCyclotomicRing n A K включается в CyclotomicField n K. Тогда это вложение инъективно: различные элементы кольца циклотоических корней соответствуют различным изображениям в циклотомическом поле.
LaTeX
$$$\\forall x,y \\,\\in\\; \\operatorname{CyclotomicRing}(n,A,K),\\; \\operatorname{algebraMap}(x) = \\operatorname{algebraMap}(y) \\Rightarrow x = y$$$
Lean4
theorem adjoin_algebra_injective : Function.Injective <| algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :=
Subtype.val_injective
