mem_coeSubmodule — Mathlib

English

An element x ∈ S lies in the image of I under the algebra map R → S if and only if there exists y ∈ I with algebraMap(y) = x.

Русский

Элемент x ∈ S принадлежит образу I под алгебраическим отображением R → S тогда и только тогда, когда существует y ∈ I с algebraMap(y) = x.

LaTeX

$$$x \\in \\operatorname{coeSubmodule}(S,I) \\iff \\exists y\\in I\\; (\\operatorname{algebraMap} R S)(y) = x$$$

Lean4

theorem mem_coeSubmodule (I : Ideal R) {x : S} : x ∈ coeSubmodule S I ↔ ∃ y : R, y ∈ I ∧ algebraMap R S y = x :=
  Iff.rfl

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