Covariant instances on WithZero

Adding a zero to a type with a preorder and multiplication which satisfies some axiom, gives us a new type which satisfies some variant of the axiom.

Example

If α satisfies b₁ < b₂ → a * b₁ < a * b₂ for all a, then WithZero α satisfies b₁ < b₂ → a * b₁ < a * b₂ for all a > 0, which is PosMulStrictMono (WithZero α).

Application

The type ℤᵐ⁰ := WithZero (Multiplicative ℤ) is used a lot in mathlib's valuation theory. These instances enable lemmas such as mul_pos to fire on ℤᵐ⁰.

instance instPosMulStrictMonoWithZeroOfMulLeftStrictMono {α : Type u_1} [Mul α] [Preorder α] [MulLeftStrictMono α] : PosMulStrictMono (WithZero α)

instance instMulPosStrictMonoWithZeroOfMulRightStrictMono {α : Type u_1} [Mul α] [Preorder α] [MulRightStrictMono α] : MulPosStrictMono (WithZero α)

instance instPosMulMonoWithZeroOfMulLeftMono {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] : PosMulMono (WithZero α)

instance instMulPosMonoWithZeroOfMulRightMono {α : Type u_1} [Mul α] [Preorder α] [MulRightMono α] : MulPosMono (WithZero α)

theorem WithZero.withZeroUnitsEquiv_strictMono {α : Type u_1} [LinearOrderedCommGroupWithZero α] : StrictMono ⇑withZeroUnitsEquiv

def OrderIso.withZeroUnits {α : Type u_1} [LinearOrderedCommGroupWithZero α] : WithZero αˣ ≃o α

Given any linearly ordered commutative group with zero α, this is the order isomorphism between WithZero αˣ with α.

Equations

• OrderIso.withZeroUnits = { toEquiv := WithZero.withZeroUnitsEquiv.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.withZeroUnits_symm_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] (a : α) : (RelIso.symm withZeroUnits) a = if h : a = 0 then 0 else ↑(Units.mk0 a h)

@[simp]

theorem OrderIso.withZeroUnits_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] (n : WithZero αˣ) : withZeroUnits n = WithZero.recZeroCoe 0 Units.val n

theorem WithZero.withZeroUnitsEquiv_symm_strictMono {α : Type u_1} [LinearOrderedCommGroupWithZero α] : StrictMono ⇑withZeroUnitsEquiv.symm