English
A variant showing that SMulCommClass β N α holds when SMulCommClass β M α holds and g: N → M is used to pull back the action.
Русский
Вариант, показывающий, что SMulCommClass β N α сохраняется, если SMulCommClass β M α выполняется и используется отображение g: N → M для переноса действия.
LaTeX
$$$ [SMul β α] \; [SMulCommClass β M α] (g : N \to M) : SMulCommClass β N α, \; smul_comm _ n := smul_comm _ (g n). $$$
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)
