instSMulWithZero

Mathlib.Algebra.GroupWithZero.Action.Hom

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

Lean4

instance [Zero M] [SMulWithZero M B] : SMulWithZero M (ZeroHom A B) where zero_smul _ := ext fun _ => zero_smul _ _

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

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

Разделы

Аффилиация

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