instMulPosStrictMonoWithZeroOfMulRightStrictMono

English

An instance that WithZero inherits MulPosStrictMono from MulRightStrictMono.

Русский

Экземпляр, где WithZero наследует MulPosStrictMono от MulRightStrictMono.

LaTeX

$$InstMulPosStrictMonoWithZeroOfMulRightStrictMono$$

Lean4

instance {α : Type*} [Mul α] [Preorder α] [MulRightStrictMono α] : MulPosStrictMono (WithZero α) where
  elim :=
    @fun
      | ⟨(x : α), hx⟩, 0, (b : α), _ => by simpa only [mul_zero] using WithZero.zero_lt_coe _
      | ⟨(x : α), hx⟩, (a : α), (b : α), h => by
        dsimp only at h ⊢
        norm_cast at h ⊢
        exact mul_lt_mul_right' h x

Похожие утверждения