span_singleton_mul_left_injective

English

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

Русский

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

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,\ I\, (\operatorname{span}\{x\})=J\,(\operatorname{span}\{x\})\ \Rightarrow\ I=J.$$$

Lean4

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

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