English
An algebra over Real restricts to an algebra over NNReal; i.e., there is an ℝ≥0-algebra structure on A compatible with the original Real-algebra structure.
Русский
Алгебра над Real ограничивается до алгебры над NNReal; существет совместимая ℝ≥0-алгебра A.
LaTeX
$$$\text{If } [Algebra\, \mathbb{R}\, A], \text{then } [Algebra\, \mathbb{R}_{\ge 0}\, A].$$$
Lean4
/-- An `Algebra` over `ℝ` restricts to an `Algebra` over `ℝ≥0`. -/
instance {A : Type*} [Semiring A] [Algebra ℝ A] : Algebra ℝ≥0 A
where
smul := (· • ·)
commutes' r x := by simp [Algebra.commutes]
smul_def' r x := by simp [← Algebra.smul_def (r : ℝ) x, smul_def]
algebraMap :=
(algebraMap ℝ A).comp
(toRealHom : ℝ≥0 →+* ℝ)
-- verify that the above produces instances we might care about
