instDistribSMul

Mathlib.Algebra.Module.Hom

URI: https://scilib.ai/kg/mathlib#AddMonoid.End.instDistribSMul

Lean4

instance instDistribSMul [DistribSMul M A] : DistribSMul M (AddMonoid.End A) :=
  AddMonoidHom.instDistribSMul

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

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

Разделы

Аффилиация

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