algebraMap_mem

Mathlib.Algebra.Algebra.Operations

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

English

For any r ∈ R, the image algebraMap(r) lies in the unit subalgebra (1) of A viewed as a SubMulAction.

Русский

Для любого r ∈ R образ algebraMap(r) лежит в единичной подподмодели (1) A как SubMulAction.

LaTeX

$$$\\text{algebraMap } R A\\, r \\in (1 : \\text{SubMulAction } R A)$$$

Lean4

theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : SubMulAction R A) :=
  ⟨r, (algebraMap_eq_smul_one r).symm⟩

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

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

Разделы

Аффилиация

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