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

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.

theorem WithZeroMulInt.toNNReal_pos_apply {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x = 0) : (toNNReal he) x = 0

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)

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.

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.

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

The map toNNReal is strictly monotone whenever 1 < e.

theorem WithZeroMulInt.toNNReal_eq_one_iff {e : NNReal} (m : WithZero (Multiplicative ℤ)) (he0 : e ≠ 0) (he1 : e ≠ 1) : (toNNReal he0) m = 1 ↔ m = 1

theorem WithZeroMulInt.toNNReal_lt_one_iff {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e) : (toNNReal ⋯) m < 1 ↔ m < 1

theorem WithZeroMulInt.toNNReal_le_one_iff {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e) : (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1