mem_span_singleton_mul — Mathlib

English

For all x,y ∈ R and ideal I, x ∈ span{y} · I iff there exists z ∈ I with y z = x.

Русский

Для любых x,y ∈ R и идеала I верно: x ∈ span{y} · I тогда и только тогда, когда существует z ∈ I такое, что y z = x.

LaTeX

$$$ x \\in \\operatorname{span}\\{y\\} \\cdot I \\iff \\exists z \\in I, y z = x $$$

Lean4

theorem mem_span_singleton_mul {x y : R} {I : Ideal R} : x ∈ span { y } * I ↔ ∃ z ∈ I, y * z = x := by
  simp only [mul_comm, mem_mul_span_singleton]

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