compHom_algebraMap_eq

Mathlib.Algebra.Algebra.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.compHom_algebraMap_eq

English

In the composed algebra, the algebra map from S to A equals the composition of algebraMap from R to A with f.

Русский

В композиционной алгебре отображение algebraMap S A равно композиции algebraMap R A и f.

LaTeX

$$$\text{algebraMap}(S,A) = (\operatorname{algebraMap}(R,A)) \circ f$$$

Lean4

theorem compHom_algebraMap_eq :
    letI := compHom A f
    algebraMap S A = (algebraMap R A).comp f :=
  rfl

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

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

Разделы

Аффилиация

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