English
If IsPretransitive M α holds, then IsPretransitive N α holds for a composition with a monoid homomorphism.
Русский
Если IsPretransitive M α выполняется, то IsPretransitive N α выполняется для композиции с гомоморфизмом моноидов.
LaTeX
$$$\\mathrm{MulAction.IsPretransitive } M α \\Rightarrow \\mathrm{MulAction.IsPretransitive } N α$ via a hom $f:M\\to* N$.$$
Lean4
/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
a multiplicative action of `N` on `α`.
See note [reducible non-instances]. -/
@[to_additive]
abbrev compHom [Monoid N] (g : N →* M) : MulAction N α
where
smul := SMul.comp.smul g
one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..
