comp

Mathlib.Algebra.Group.Action.Defs

URI: https://scilib.ai/kg/mathlib#SMul.comp

Lean4

/-- An action of `M` on `α` and a function `N → M` induces an action of `N` on `α`. -/
-- See note [reducible non-instances]
-- Since this is reducible, we make sure to go via
-- `SMul.comp.smul` to prevent typeclass inference unfolding too far

@[to_additive /-- An additive action of `M` on `α` and a function `N → M` induces an additive
    action of `N` on `α`. -/
    ]
abbrev comp (g : N → M) : SMul N α where smul := SMul.comp.smul g

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

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

Разделы

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

Аффилиация

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