Coercion from ℕ∞
to ℝ≥0∞
#
In this file we define a coercion from ℕ∞
to ℝ≥0∞
and prove some basic lemmas about this map.
@[simp]
Coercion ℕ∞ → ℝ≥0∞
as an OrderEmbedding
.
Instances For
Coercion ℕ∞ → ℝ≥0∞
as a ring homomorphism.
Instances For
@[simp]