algebraMap_mem

Mathlib.Algebra.Algebra.Subalgebra.Basic

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

English

The image of any scalar under the algebra map lies in the subalgebra S.

Русский

Образ любого скалярного элемента под алгебраMap принадлежит подалгебре S.

LaTeX

$$$\mathrm{algebraMap}(R,A)(r) \in S$ for all $r \in R$$$

Lean4

protected theorem algebraMap_mem (r : R) : algebraMap R A r ∈ S :=
  algebraMap_mem S r

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

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

Разделы

Аффилиация

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