instDistribMulActionOfReal — Mathlib

English

A distributive action of Real on a type M restricts to a distributive action of NNReal on M by restricting scalars via the Real inclusion.

Русский

Дистрибутивное действие Real на M ограничивается до дистрибутивного действия NNReal на M посредством вложения Real.

LaTeX

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

Lean4

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

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