English
Given SMul β α and SMulCommClass M β α, the map g: N → M yields SMulCommClass N β α, with smul_comm n := smul_comm (g n).
Русский
Имея SMul β α и SMulCommClass M β α, отображение g: N → M даёт SMulCommClass N β α; выполняется smul_comm n = smul_comm (g n).
LaTeX
$$$ [SMul \beta \alpha] \; [SMulCommClass M \beta \alpha] (g : N \to M) : SMulCommClass N \beta \alpha, \text{ где } smul\_comm n := smul\_comm (g\,n). $$$
Lean4
/-- Given a tower of scalar actions `M → α → β`, if we use `SMul.comp`
to pull back both of `M`'s actions by a map `g : N → M`, then we obtain a new
tower of scalar actions `N → α → β`.
This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
@[to_additive /-- Given a tower of additive actions `M → α → β`, if we use `SMul.comp` to pull back both of
`M`'s actions by a map `g : N → M`, then we obtain a new tower of scalar actions `N → α → β`.
This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
]
theorem isScalarTower [SMul M β] [SMul α β] [IsScalarTower M α β] (g : N → M) : by haveI := comp α g; haveI := comp β g;
exact IsScalarTower N α β where
__ := comp α g
__ := comp β g
smul_assoc n := smul_assoc (g n)
