rat — Mathlib

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

Похожие утверждения