mem_colon_singleton — Mathlib

English

For any submodule N of a module M and any x ∈ M, r ∈ I.colon(span{x}) iff r • x ∈ I for an ideal I.

Русский

Для идеала I и подмодуля N ⊆ M справедливо: r ∈ I.colon(span{x}) тогда и только тогда, когда r·x ∈ I.

LaTeX

$$$ r \\in I : \\mathrm{span}\\,\\{ x \\} \\iff r \\cdot x \\in I $$$

Lean4

@[simp]
theorem _root_.Ideal.mem_colon_singleton {I : Ideal R} {x r : R} : r ∈ I.colon (Ideal.span { x }) ↔ r * x ∈ I := by
  simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]

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