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 (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] : PosMulStrictMono (WithZero α)

Equations

• ⋯ = ⋯

instance instMulPosStrictMonoWithZeroOfCovariantClassSwapHMulLt {α : Type u_1} [Mul α] [Preorder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] : MulPosStrictMono (WithZero α)

Equations

• ⋯ = ⋯

instance instPosMulMonoWithZeroOfCovariantClassHMulLe {α : Type u_1} [Mul α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : PosMulMono (WithZero α)

Equations

• ⋯ = ⋯

instance instMulPosMonoWithZeroOfCovariantClassSwapHMulLe {α : Type u_1} [Mul α] [Preorder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : MulPosMono (WithZero α)

Equations

• ⋯ = ⋯