algebraMap_mem

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.algebraMap_mem

English

x ∈ (1 : Submodule R A) iff ∃ y with algebraMap R A y = x.

Русский

x ∈ (1 : Submodule R A) тогда и только тогда, когда ∃ y: R, algebraMap R A y = x.

LaTeX

$$$ x \in (1 : Submodule R A) \iff \exists y, \ algebraMap R A y = x. $$$

Lean4

theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) := by simp [one_eq_range]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru