mem_div_iff_smul_subset — Mathlib

English

For submodules I,J of A, an element x lies in the quotient I/J precisely when multiplying x by J yields a subset of I.

Русский

Для подмодулей I и J подмодуля A: элемент x принадлежит I/J тогда и только тогда, когда произведение x на J лежит в I.

LaTeX

$$$x \\in I/J \\iff x \\cdot J \\subseteq I$$$

Lean4

theorem mem_div_iff_smul_subset {x : A} {I J : Submodule R A} : x ∈ I / J ↔ x • (J : Set A) ⊆ I :=
  ⟨fun h y ⟨y', hy', xy'_eq_y⟩ => by rw [← xy'_eq_y]; exact h _ hy', fun h _ hy => h (Set.smul_mem_smul_set hy)⟩

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