smulZeroClass

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#ZeroHom.smulZeroClass

Lean4

/-- Pushforward a zero-preserving scalar multiplication along a zero-preserving map.
See note [reducible non-instances]. -/
protected abbrev smulZeroClass [Zero B] [SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
    SMulZeroClass M B where smul_zero c := by rw [← map_zero f, ← smul, smul_zero]

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

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

Разделы

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

Аффилиация

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