coe_algebraMap

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#SubalgebraClass.coe_algebraMap

English

The algebra map from R into S via the subalgebra equals the algebra map into A when viewed in A.

Русский

Алгебраическая карта из R в S через подалгебру равна карте в A при рассмотрении в A.

LaTeX

$$$(algebraMap R S r) = algebraMap R A r$ for all $r \in R$$$

Lean4

@[simp, norm_cast]
theorem coe_algebraMap (r : R) : (algebraMap R s r : A) = algebraMap R A r :=
  rfl

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

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

Разделы

Аффилиация

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