English
If A is a Semiring with an ENNReal-algebra structure, then A inherits an NNReal-algebra structure by composing the ENNReal-algebra map with the natural inclusion of NNReal into ENNReal.
Русский
Если A — полукольцо с ENNReal-алгеброй, то A наследует NNReal-алгебрe через композицию алгебраической карты ENNReal с естественным включением NNReal в ENNReal.
LaTeX
$$$\text{Algebra}_{\mathbb{R}_{\ge 0}}(A)\text{ with } \operatorname{algebraMap}_{\mathbb{R}_{\ge 0}} = (\operatorname{algebraMap}_{\mathbb{R}_{\ge 0}^\infty}) \circ (\operatorname{ofNNRealHom}).$$$
Lean4
/-- An `Algebra` over `ℝ≥0∞` restricts to an `Algebra` over `ℝ≥0`. -/
noncomputable instance {A : Type*} [Semiring A] [Algebra ℝ≥0∞ A] : Algebra ℝ≥0 A
where
smul := (· • ·)
commutes' r x := by simp [Algebra.commutes]
smul_def' r x := by simp [← Algebra.smul_def (r : ℝ≥0∞) x, smul_def]
algebraMap :=
(algebraMap ℝ≥0∞ A).comp
(ofNNRealHom : ℝ≥0 →+* ℝ≥0∞)
-- verify that the above produces instances we might care about
