English
Transfer a MulAction across an Equiv: if e: α ≃ β and β has a MulAction of M, then α inherits a MulAction of M via the equivalence, with action defined by the pullback along e.
Русский
Переносим действие через эквивалент: если e: α ≃ β и β имеет действие M, то α получает действие M через эквивалент, задаваемое переносом действия обратно по e.
LaTeX
$$$\text{Equiv.mulAction } M e: α \to α \text{ is a MulAction whenever } [MulAction M β].$$$
Lean4
/-- Transfer `MulAction` across an `Equiv` -/
@[to_additive /-- Transfer `AddAction` across an `Equiv` -/
]
protected abbrev mulAction (e : α ≃ β) [MulAction M β] : MulAction M α
where
__ := e.smul M
one_smul := by simp [smul_def]
mul_smul := by simp [smul_def, mul_smul]
