instDistribMulAction

Mathlib.Algebra.Lie.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#LieDerivation.instDistribMulAction

English

The coercion of D via coeFnAddMonoidHom agrees with its value as an element: coeFnAddMonoidHom D = D.

Русский

Приведение через coeFnAddMonoidHom согласуется с самим элементом: coeFnAddMonoidHom D = D.

LaTeX

$$$\text{coeFnAddMonoidHom } D = D$$$

Lean4

instance : DistribMulAction S (LieDerivation R L M) :=
  Function.Injective.distribMulAction coeFnAddMonoidHom coe_injective coe_smul

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

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

Разделы

Аффилиация

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