instIsScalarTowerNNReal — Mathlib

English

There is a scalar tower structure from NNReal through ENNReal to M and N, i.e., smul_assoc holds compatibly.

Русский

Существует структура башни скаляров NNReal → ENNReal → M, обеспечивающая совместимость умножения.

LaTeX

$$$\\text{IsScalarTower NNReal M N}$$$

Lean4

instance {M N : Type*} [MulAction ℝ≥0∞ M] [MulAction ℝ≥0∞ N] [SMul M N] [IsScalarTower ℝ≥0∞ M N] : IsScalarTower ℝ≥0 M N
    where smul_assoc r := smul_assoc (r : ℝ≥0∞)

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