span_singleton_mul_le_iff — Mathlib

English

Equivalent reformulation with I ≤ span{x} · J iff ∀ z ∈ I, ∃ zJ ∈ J with x zJ = z.

Русский

Эквивалентная формулировка: I ≤ span{x} · J эквивалентно ∀ z ∈ I, ∃ zJ ∈ J: x zJ = z.

LaTeX

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

Lean4

theorem span_singleton_mul_le_iff {x : R} {I J : Ideal R} : span { x } * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J :=
  by
  simp only [mul_le, mem_span_singleton]
  constructor
  · intro h zI hzI
    exact h x (dvd_refl x) zI hzI
  · rintro h _ ⟨z, rfl⟩ zI hzI
    rw [mul_comm x z, mul_assoc]
    exact J.mul_mem_left _ (h zI hzI)

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