English
Given compatible actions, the pullback of a multiplicative distributive action along an injective map preserves the Smul-commutation: the resulting structure has SMul-commutativity.
Русский
При совместимых действиях перенос мультидистрибутной действия вдоль инъекции сохраняет совместимость умножения-скаляра.
LaTeX
$$$$\text{smulCommClass}' \;\to\; \text{SMulCommClass } β N α \; \text{via } comp\, α\, g.$$$$
Lean4
/-- This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
@[to_additive /-- This cannot be an instance because it can cause infinite loops whenever the `VAdd` arguments
are still metavariables. -/
]
theorem smulCommClass' [SMul β α] [SMulCommClass β M α] (g : N → M) :
haveI := comp α g
SMulCommClass β N α
where
__ := comp α g
smul_comm _ n := smul_comm _ (g n)
