Theorems · Theorem · order theory

WithTop.mul_left_strictMono

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithTop α} [inst_2 : Preorder α]
  [MulPosStrictMono α], 0 < a → a ≠ ⊤ → StrictMono fun x => x * a

Defined in

Mathlib.Algebra.Order.Ring.WithTop

Cited by

2 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqMulZeroClassPreorderMulPosStrictMono