distribSMulLeft

Mathlib.Algebra.GroupWithZero.Action.Defs

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

Lean4

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

See also `Function.Surjective.distribMulActionLeft`.
-/
abbrev distribSMulLeft {R S M : Type*} [AddZeroClass M] [DistribSMul R M] [SMul S M] (f : R → S)
    (hf : Function.Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribSMul S M :=
  { hf.smulZeroClassLeft f hsmul with smul_add := hf.forall.mpr fun c x y => by simp only [hsmul, smul_add] }

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

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

Разделы

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

Аффилиация

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