Commit 2024-10-04 14:05 6039b328

feat(Data/Int/WithZero): add WithZeroMultIntToNNReal (#15741) We define the morphism withZeroMultIntToNNReal from ℤₘ₀ → ℝ≥0 sending 0 ↦ 0 and x ↦ e^(Multiplicative.toAdd (WithZero.unzero hx) when x ≠ 0, for a nonzero e : ℝ≥0 and prove some of its properties.