toGmodule

Mathlib.Algebra.Module.GradedModule

URI: https://scilib.ai/kg/mathlib#DirectSum.GSemiring.toGmodule

Lean4

/-- A graded version of `Semiring.toModule`. -/
instance toGmodule [AddMonoid ιA] [∀ i : ιA, AddCommMonoid (A i)] [h : GSemiring A] : Gmodule A A :=
  { GMonoid.toGMulAction A with
    smul_add := fun _ _ _ => h.mul_add _ _ _
    smul_zero := fun _ => h.mul_zero _
    add_smul := fun _ _ => h.add_mul _ _
    zero_smul := fun _ => h.zero_mul _ }

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

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

Разделы

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

Аффилиация

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