instModuleNNReal — Mathlib

English

Let M be an AddCommMonoid with a module structure over ENNReal. Then M becomes a module over NNReal by restricting scalars along the inclusion NNReal → ENNReal.

Русский

Пусть M — коммутативный аддитивный моиум с модульной структурой над ENNReal. Тогда M образует модуль над NNReal путем ограничения скаляров по включению NNReal → ENNReal.

LaTeX

$$$\text{Module}_{\mathbb{R}_{\ge 0}}(M)\text{ with } r \cdot m := (\operatorname{ofNNReal} r) \cdot m.$$$

Lean4

/-- A `Module` over `ℝ≥0∞` restricts to a `Module` over `ℝ≥0`. -/
noncomputable instance {M : Type*} [AddCommMonoid M] [Module ℝ≥0∞ M] : Module ℝ≥0 M :=
  Module.compHom M ofNNRealHom

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