mulAction

Mathlib.Algebra.GradedMonoid

URI: https://scilib.ai/kg/mathlib#GradedMonoid.GradeZero.mulAction

Lean4

/-- Each grade `A i` derives an `A 0`-action structure from `GMonoid A`. -/
instance mulAction {i} : MulAction (A 0) (A i) :=
  letI := MulAction.compHom (GradedMonoid A) (mkZeroMonoidHom A)
  Function.Injective.mulAction (mk i) sigma_mk_injective mk_zero_smul

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

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

Разделы

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

Аффилиация

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