English
There is IsScalarTower Rat → R → M for rings R and modules M; i.e., (r)•(x)•y = r•(x•y) for r ∈ Rat, x ∈ R, y ∈ M.
Русский
Существует IsScalarTower Rat → R → M: (r)•(x)•y = r•(x•y) для r ∈ Rat, x ∈ R, y ∈ M.
LaTeX
$$$(r : \\mathrm{Rat}) \\cdot (x \\cdot y) = (r \\cdot x) \\cdot y$$$
Lean4
instance rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module ℚ R] [Module ℚ M] :
IsScalarTower ℚ R M where smul_assoc r x y := map_rat_smul ((smulAddHom R M).flip y) r x