compHom_smul_def

Mathlib.Algebra.Algebra.Defs

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

English

This is a definitional equality: the smul in the composed algebra is definably the image under f.

Русский

Это определение: смул в композиции алгебр задаётся образом через f.

LaTeX

$$$s \cdot x = f(s) \cdot x$$$

Lean4

theorem compHom_smul_def (s : S) (x : A) :
    letI := compHom A f
    s • x = f s • x :=
  rfl

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

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

Разделы

Аффилиация

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