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 α)