instAddZeroClass

Mathlib.GroupTheory.GroupAction.Hom

URI: https://scilib.ai/kg/mathlib#MulActionHom.instAddZeroClass

Lean4

instance [SMul M X] [AddZeroClass Y] [DistribSMul N Y] : AddZeroClass (X →ₑ[σ] Y)
    where
  add f g := ⟨f + g, by simp [smul_add]⟩
  zero_add _ := ext fun _ ↦ zero_add _
  add_zero _ := ext fun _ ↦ add_zero _

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

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

Разделы

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

Аффилиация

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