English
If E is an additive commutative monoid with a star operation, and E is a module over the real numbers with a compatible star-structure, then E becomes a star-module over NNReal (the nonnegative reals) by restricting scalars; i.e. for all r in NNReal and all x in E, (r · x)★ = r · x★.
Русский
Если E — абелево-приводимый по сложению моноид с операцией звезды и E — модуль над ℝ с совместимой структурой звезды, то E наследует звёздную структуру-как модуль над NNReal (неотрицательными вещественными числами): для всех r ∈ ℝ≥0 и x ∈ E выполняется (r · x)★ = r · x★.
LaTeX
$$$\forall E$ a (AddCommMonoid E) with (Star E) and (Module \mathbb{R} E) and (StarModule \mathbb{R} E),\; (\forall r \in \mathbb{R}_{\ge 0}, \forall x \in E),\; (r \cdot x)^{*} = r \cdot x^{*}. $$$
Lean4
instance {E : Type*} [AddCommMonoid E] [Star E] [Module ℝ E] [StarModule ℝ E] : StarModule ℝ≥0 E where
star_smul _ := star_smul (_ : ℝ)
