nnrat — Mathlib

English

There is an IsScalarTower ℚ≥0 → R → M for any appropriate R and M, i.e., (r)•(x)•y = r•(x•y) for r ∈ ℚ≥0, x ∈ R, y ∈ M.

Русский

Существует IsScalarTower ℚ≥0 → R → M: (r)•(x)•y = r•(x•y) для r ∈ ℚ≥0, x ∈ R, y ∈ M.

LaTeX

$$$(r : \\mathbb{Q}_{\\ge 0}) \\cdot x \\cdot y = r \\cdot (x \\cdot y)$$$

Lean4

instance nnrat {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module ℚ≥0 R] [Module ℚ≥0 M] :
    IsScalarTower ℚ≥0 R M where smul_assoc r x y := map_nnrat_smul ((smulAddHom R M).flip y) r x

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