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
instPosMulStrictMonoWithZeroOfCovariantClassHMulLt
{α : Type u_1}
[Mul α]
[Preorder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2]
:
Equations
- ⋯ = ⋯
instance
instMulPosStrictMonoWithZeroOfCovariantClassSwapHMulLt
{α : Type u_1}
[Mul α]
[Preorder α]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2]
:
Equations
- ⋯ = ⋯
instance
instPosMulMonoWithZeroOfCovariantClassHMulLe
{α : Type u_1}
[Mul α]
[Preorder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
:
PosMulMono (WithZero α)
Equations
- ⋯ = ⋯
instance
instMulPosMonoWithZeroOfCovariantClassSwapHMulLe
{α : Type u_1}
[Mul α]
[Preorder α]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
:
MulPosMono (WithZero α)
Equations
- ⋯ = ⋯