mulDistribMulAction'

Mathlib.Algebra.Module.ULift

URI: https://scilib.ai/kg/mathlib#ULift.mulDistribMulAction'

Lean4

instance mulDistribMulAction' [Monoid R] [Monoid M] [MulDistribMulAction R M] : MulDistribMulAction R (ULift M) :=
  {
    ULift.mulAction' with
    smul_one := fun _ => by
      ext
      simp [smul_one]
    smul_mul := fun _ _ _ => by
      ext
      simp [smul_mul'] }

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

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

Разделы

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

Аффилиация

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