span_singleton_mul_le_span_singleton_mul

English

If R is a domain and x ≠ 0, then span{x} · I ≤ span{x} · J iff I ≤ J.

Русский

Если R — домен и x ≠ 0, то span{x} · I ≤ span{x} · J тогда и только тогда, когда I ≤ J.

LaTeX

$$$ [IsDomain\\, R] \\{x : R\\} (x \\neq 0) : I \\cdot \\operatorname{span}\\{x\\} ≤ J \\cdot \\operatorname{span}\\{x\\} \\iff I ≤ J $$$

Lean4

theorem span_singleton_mul_le_span_singleton_mul {x y : R} {I J : Ideal R} :
    span { x } * I ≤ span { y } * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ := by
  simp only [span_singleton_mul_le_iff, mem_span_singleton_mul, eq_comm]

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