algebraMap_mem

Mathlib.Algebra.Star.Subalgebra

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

English

For every r in R, the image algebraMap(R,A)(r) lies in S.

Русский

Для каждого r в R образ algebraMap(R,A)(r) принадлежит S.

LaTeX

$$$\mathsf{algebraMap}\,R\,A\; r \in S$$$

Lean4

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

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

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

Разделы

Аффилиация

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