smulWithZero

Mathlib.Algebra.DirectSum.Ring

URI: https://scilib.ai/kg/mathlib#DirectSum.GradeZero.smulWithZero

Lean4

instance smulWithZero (i : ι) : SMulWithZero (A 0) (A i) :=
  by
  letI := SMulWithZero.compHom (⨁ i, A i) (of A 0).toZeroHom
  exact Function.Injective.smulWithZero (of A i).toZeroHom DFinsupp.single_injective (of_zero_smul A)

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

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

Разделы

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

Аффилиация

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