THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define a coercion from
ℝ≥0∞ and prove some basic lemmas about this map.
ℕ∞ → ℝ≥0∞ as a ring homomorphism.