span_singleton_mul_right_injective

English

Let R be an integral domain and x ∈ R with x ≠ 0. The map I ↦ (span {x}) · I from ideals to ideals is injective.

Русский

Пусть R — целостный домен, x ∈ R, x ≠ 0. Отображение I ↦ (span {x}) · I от идеалов в идеалы инъективно.

LaTeX

$$$\\text{Let }R\\text{ be an integral domain and }x\\in R\\text{ with }x\\neq 0.\\ For\\ all\\ ideals\\ I,J\\subseteq R,\\ (\\operatorname{span}\\{x\\})I=(\\operatorname{span}\\{x\\})J\\ \\Rightarrow\\ I=J.$$$

Lean4

theorem span_singleton_mul_right_injective [IsDomain R] {x : R} (hx : x ≠ 0) :
    Function.Injective ((span { x } : Ideal R) * ·) := fun _ _ => (span_singleton_mul_right_inj hx).mp

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