smulZeroClassLeft

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#Function.Surjective.smulZeroClassLeft

Lean4

/-- Push forward the multiplication of `R` on `M` along a compatible surjective map `f : R → S`.

See also `Function.Surjective.distribMulActionLeft`.
-/
abbrev smulZeroClassLeft {R S M : Type*} [Zero M] [SMulZeroClass R M] [SMul S M] (f : R → S)
    (hf : Function.Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) : SMulZeroClass S M
    where
  smul := (· • ·)
  smul_zero := hf.forall.mpr fun c => by rw [hsmul, smul_zero]

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

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

Разделы

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

Аффилиация

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