instIsCentralScalar

Mathlib.Algebra.GroupWithZero.Action.Hom

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.instIsCentralScalar

← MathLib Explorer

English

AddMonoidHom A B is central under M-action: IsCentralScalar M (A →+ B).

Русский

AddMonoidHom A B находится в центре относительно действия M: IsCentralScalar M (A →+ B).

LaTeX

$$[IsCentralScalar M (A →+ B)]$$

Lean4

instance [DistribSMul M B] [DistribSMul Mᵐᵒᵖ B] [IsCentralScalar M B] : IsCentralScalar M (A →+ B) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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