instMulActionWithZero

Mathlib.Algebra.GroupWithZero.Action.Hom

URI: https://scilib.ai/kg/mathlib#ZeroHom.instMulActionWithZero

Lean4

instance [MonoidWithZero M] [MulActionWithZero M B] : MulActionWithZero M (ZeroHom A B)
    where
  __ : SMulWithZero _ _ := inferInstance
  one_smul _ := ext fun _ => one_smul _ _
  mul_smul _ _ _ := ext fun _ => mul_smul _ _ _

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

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

Разделы

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

Аффилиация

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