Documentation

Mathlib.Algebra.Order.GroupWithZero.WithZero

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 ℤᵐ⁰.

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

Equations
Instances For
    @[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)