toAlgHom_apply

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#IsScalarTower.toAlgHom_apply

English

Equality of the two canonical algebra maps to A from the tower.

Русский

Равенство двух канонических алгебраических отображений в A из башни.

LaTeX

$$$\mathrm{toAlgHom}\;R\;S\;A\;y = \mathrm{algebraMap}\;S\;A\;(\mathrm{algebraMap}\;R\;S\;y)$$$

Lean4

theorem toAlgHom_apply (y : S) : toAlgHom R S A y = algebraMap S A y :=
  rfl

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

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

Разделы

Аффилиация

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