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 α]
:
instance
instMulPosStrictMonoWithZeroOfMulRightStrictMono
{α : Type u_1}
[Mul α]
[Preorder α]
[MulRightStrictMono α]
:
instance
instPosMulMonoWithZeroOfMulLeftMono
{α : Type u_1}
[Mul α]
[Preorder α]
[MulLeftMono α]
:
PosMulMono (WithZero α)
instance
instMulPosMonoWithZeroOfMulRightMono
{α : Type u_1}
[Mul α]
[Preorder α]
[MulRightMono α]
:
MulPosMono (WithZero α)
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' := ⋯ }
Instances For
@[simp]
theorem
OrderIso.withZeroUnits_symm_apply
{α : Type u_1}
[LinearOrderedCommGroupWithZero α]
(a : α)
:
@[simp]
theorem
OrderIso.withZeroUnits_apply
{α : Type u_1}
[LinearOrderedCommGroupWithZero α]
(n : WithZero αˣ)
: