le_span_singleton_mul_iff — Mathlib

English

I ≤ span{x} · J iff for all zI ∈ I there exists zJ ∈ J with x zJ = zI.

Русский

I ≤ span{x} · J эквивалентно: для каждого zI ∈ I существует zJ ∈ J такое, что x zJ = zI.

LaTeX

$$$ I \\le \\operatorname{span}\\{x\\} \\cdot J \\iff \\forall zI \\in I, \\exists zJ \\in J, x \\cdot zJ = zI $$$

Lean4

theorem le_span_singleton_mul_iff {x : R} {I J : Ideal R} : I ≤ span { x } * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI :=
  show (∀ {zI} (_ : zI ∈ I), zI ∈ span { x } * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI by
    simp only [mem_span_singleton_mul]

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