compHom_algebraMap_apply

Mathlib.Algebra.Algebra.Defs

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

English

For s in S, the image algebraMap S A s equals algebraMap R A applied to f(s).

Русский

Для s ∈ S образ algebraMap S A s равен algebraMap R A (f(s)).

LaTeX

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

Lean4

theorem compHom_algebraMap_apply (s : S) :
    letI := compHom A f
    algebraMap S A s = (algebraMap R A) (f s) :=
  rfl

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

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

Разделы

Аффилиация

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