instModuleOfReal — Mathlib

English

A module over Real restricts to a module over NNReal by restricting scalars along the Real inclusion.

Русский

Модуль над Real ограничивается до модуля над NNReal через ограничение скаляров по вложению Real.

LaTeX

$$$\text{If } [Module\, \mathbb{R}\, M],\ \text{then } [Module\, \mathbb{R}_{\ge 0}\, M].$$$

Lean4

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

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