# WithZero #

In this file we provide some basic API lemmas for the `WithZero` construction and we define the morphism `WithZeroMultInt.toNNReal`.

## Main Definitions #

- `WithZeroMultInt.toNNReal` : The `MonoidWithZeroHom` from `ℤᵐ⁰ → ℝ≥0` sending `0 ↦ 0` and `x ↦ e^((WithZero.unzero hx).toAdd)` when `x ≠ 0`, for a nonzero `e : ℝ≥0`.

## Main Results #

- `WithZeroMultInt.toNNReal_strictMono` : The map `withZeroMultIntToNNReal` is strictly monotone whenever `1 < e`.

## Tags #

WithZero, multiplicative, nnreal

source
def WithZeroMulInt.toNNReal {e : NNReal} (he : e ≠ 0) :
WithZero (Multiplicative ℤ) →*₀ NNReal

Given a nonzero `e : ℝ≥0`, this is the map `ℤᵐ⁰ → ℝ≥0` sending `0 ↦ 0` and `x ↦ e^(WithZero.unzero hx).toAdd` when `x ≠ 0` as a `MonoidWithZeroHom`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem WithZeroMulInt.toNNReal_pos_apply {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x = 0) :
(toNNReal he) x = 0
source
theorem WithZeroMulInt.toNNReal_neg_apply {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) :
(toNNReal he) x = e ^ Multiplicative.toAdd (WithZero.unzero hx)
source
theorem WithZeroMulInt.toNNReal_ne_zero {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : e ≠ 0) (hm : m ≠ 0) :
(toNNReal he) m ≠ 0

`toNNReal` sends nonzero elements to nonzero elements.

source
theorem WithZeroMulInt.toNNReal_pos {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : e ≠ 0) (hm : m ≠ 0) :
0 < (toNNReal he) m

`toNNReal` sends nonzero elements to positive elements.

source
theorem WithZeroMulInt.toNNReal_strictMono {e : NNReal} (he : 1 < e) :
StrictMono ⇑(toNNReal ⋯)

The map `toNNReal` is strictly monotone whenever `1 < e`.

source
theorem WithZeroMulInt.toNNReal_eq_one_iff {e : NNReal} (m : WithZero (Multiplicative ℤ)) (he0 : e ≠ 0) (he1 : e ≠ 1) :
(toNNReal he0) m = 1 ↔ m = 1
source
theorem WithZeroMulInt.toNNReal_lt_one_iff {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e) :
(toNNReal ⋯) m < 1 ↔ m < 1
source
theorem WithZeroMulInt.toNNReal_le_one_iff {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e) :
(toNNReal ⋯) m ≤ 1 ↔ m ≤ 1