English
If a type M carries a MulAction of ℝ, then M naturally carries a MulAction of ℝ≥0 by restricting scalars via the inclusion ℝ≥0 → ℝ; specifically, c · x := (c : ℝ) · x.
Русский
Пусть множество M имеет действие умножения на ℝ; тогда на M естественным образом действует ℝ≥0, получаемое ограничением скаляров через вложение ℝ≥0 → ℝ: так что для c ∈ ℝ≥0 и x ∈ M выполняется c · x = (c : ℝ) · x.
LaTeX
$$$\text{If } M\text{ has a MulAction }\mathbb{R}\text{ on }M,\ \text{then } M\text{ has a MulAction }\mathbb{R}_{\ge 0}^M\text{ defined by } c\cdot x = (c:\mathbb{R})\cdot x.$$$
Lean4
/-- A `MulAction` over `ℝ` restricts to a `MulAction` over `ℝ≥0`. -/
instance {M : Type*} [MulAction ℝ M] : MulAction ℝ≥0 M :=
MulAction.compHom M toRealHom.toMonoidHom
