mem_mul_span_singleton — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_mul_span_singleton {x y : R} {I : Ideal R} : x ∈ I * span { y } ↔ ∃ z ∈ I, z * y = x :=
  Submodule.mem_smul_span_singleton

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