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^(Multiplicative.toAdd (WithZero.unzero hx) 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^(Multiplicative.toAdd (WithZero.unzero hx) 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) : (WithZeroMulInt.toNNReal he) x = 0

theorem WithZeroMulInt.toNNReal_neg_apply {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) : (WithZeroMulInt.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) : (WithZeroMulInt.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 < (WithZeroMulInt.toNNReal he) m

toNNReal sends nonzero elements to positive elements.

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

The map toNNReal is strictly monotone whenever 1 < e.