toGrindIntModule

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#AddCommGroup.toGrindIntModule

Lean4

instance toGrindIntModule [s : AddCommGroup α] : Grind.IntModule α :=
  { s with
    nsmul := ⟨s.nsmul⟩
    zsmul := ⟨s.zsmul⟩
    zero_zsmul := SubNegMonoid.zsmul_zero'
    one_zsmul := one_zsmul
    add_zsmul n m a := add_zsmul a n m
    zsmul_natCast_eq_nsmul n a := by simp }

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

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

Разделы

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

Аффилиация

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