English
For x ∈ R and Ideals I,J, I = span{x} · J if and only if (i) every element of I is x times some element of J, and (ii) every x-times element of J lies in I.
Русский
Пусть x ∈ R и идеалы I,J. Тогда I = span{x} · J тогда и только тогда, когда (i) каждый элемент I записывается как x умноженное на элемент из J, и (ii) x·z являетcя элементом I для любого z ∈ J.
LaTeX
$$$I=\operatorname{span}\{x\} \cdot J\iff\Big(\forall z_I\in I,\exists z_J\in J,\ x z_J=z_I\Big) \land \Big(\forall z\in J,\ x z\in I\Big)$$$
Lean4
theorem eq_span_singleton_mul {x : R} (I J : Ideal R) :
I = span { x } * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I := by
simp only [le_antisymm_iff, le_span_singleton_mul_iff, span_singleton_mul_le_iff]
