compHom

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#MulActionWithZero.compHom

Lean4

/-- Compose a `MulActionWithZero` with a `MonoidWithZeroHom`, with action `f r' • m` -/
def compHom (f : M₀' →*₀ M₀) : MulActionWithZero M₀' A
    where
  __ := SMulWithZero.compHom A f.toZeroHom
  mul_smul r s m := by change f (r * s) • m = f r • f s • m; simp [mul_smul]
  one_smul m := by change f 1 • m = m; simp

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

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

Разделы

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

Аффилиация

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