Documentation

Mathlib.Algebra.Order.GroupWithZero.Unbundled

Monotonicity of multiplication by positive elements #

This file defines typeclasses to reason about monotonicity of the operations

We use eight typeclasses to encode the various properties we care about for those two operations. These typeclasses are meant to be mostly internal to this file, to set up each lemma in the appropriate generality.

Less granular typeclasses like OrderedAddCommMonoid, LinearOrderedField should be enough for most purposes, and the system is set up so that they imply the correct granular typeclasses here. If those are enough for you, you may stop reading here! Else, beware that what follows is a bit technical.

Definitions #

In all that follows, α is an orders which has a 0 and a multiplication. Note however that we do not use lawfulness of this action in most of the file. Hence * should be considered here as a mostly arbitrary function α → α → α.

We use the following four typeclasses to reason about left multiplication (b ↦ a * b):

We use the following four typeclasses to reason about right multiplication (a ↦ a * b):

Implications #

As α gets more and more structure, those typeclasses end up being equivalent. The commonly used implications are:

Further, the bundled non-granular typeclasses imply the granular ones like so:

All these are registered as instances, which means that in practice you should not worry about these implications. However, if you encounter a case where you think a statement is true but not covered by the current implications, please bring it up on Zulip!

Notation #

The following is local notation in this file:

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/notation.20for.20positive.20elements for a discussion about this notation, and whether to enable it globally (note that the notation is currently global but broken, hence actually only works locally).

Local notation for the nonnegative elements of a type α. TODO: actually make local.

Equations
Instances For

    Local notation for the positive elements of a type α. TODO: actually make local.

    Equations
    Instances For
      @[reducible, inline]
      abbrev PosMulMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

      Typeclass for monotonicity of multiplication by nonnegative elements on the left, namely b₁ ≤ b₂ → a * b₁ ≤ a * b₂ if 0 ≤ a.

      You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSemiring.

      Equations
      Instances For
        @[reducible, inline]
        abbrev MulPosMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

        Typeclass for monotonicity of multiplication by nonnegative elements on the right, namely a₁ ≤ a₂ → a₁ * b ≤ a₂ * b if 0 ≤ b.

        You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSemiring.

        Equations
        Instances For
          @[reducible, inline]
          abbrev PosMulStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

          Typeclass for strict monotonicity of multiplication by positive elements on the left, namely b₁ < b₂ → a * b₁ < a * b₂ if 0 < a.

          You should usually not use this very granular typeclass directly, but rather a typeclass like StrictOrderedSemiring.

          Equations
          Instances For
            @[reducible, inline]
            abbrev MulPosStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

            Typeclass for strict monotonicity of multiplication by positive elements on the right, namely a₁ < a₂ → a₁ * b < a₂ * b if 0 < b.

            You should usually not use this very granular typeclass directly, but rather a typeclass like StrictOrderedSemiring.

            Equations
            Instances For
              @[reducible, inline]
              abbrev PosMulReflectLT (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

              Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on the left, namely a * b₁ < a * b₂ → b₁ < b₂ if 0 ≤ a.

              You should usually not use this very granular typeclass directly, but rather a typeclass like LinearOrderedSemiring.

              Equations
              Instances For
                @[reducible, inline]
                abbrev MulPosReflectLT (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

                Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on the right, namely a₁ * b < a₂ * b → a₁ < a₂ if 0 ≤ b.

                You should usually not use this very granular typeclass directly, but rather a typeclass like LinearOrderedSemiring.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev PosMulReflectLE (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

                  Typeclass for reverse monotonicity of multiplication by positive elements on the left, namely a * b₁ ≤ a * b₂ → b₁ ≤ b₂ if 0 < a.

                  You should usually not use this very granular typeclass directly, but rather a typeclass like LinearOrderedSemiring.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev MulPosReflectLE (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

                    Typeclass for reverse monotonicity of multiplication by positive elements on the right, namely a₁ * b ≤ a₂ * b → a₁ ≤ a₂ if 0 < b.

                    You should usually not use this very granular typeclass directly, but rather a typeclass like LinearOrderedSemiring.

                    Equations
                    Instances For
                      instance PosMulMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulMono α] :
                      CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x x_1
                      Equations
                      • =
                      instance MulPosMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosMono α] :
                      CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x x_1
                      Equations
                      • =
                      instance PosMulReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] :
                      ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x < x_1
                      Equations
                      • =
                      instance MulPosReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] :
                      ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x < x_1
                      Equations
                      • =
                      theorem mul_le_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] (h : b c) (a0 : 0 a) :
                      a * b a * c
                      theorem mul_le_mul_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] (h : b c) (a0 : 0 a) :
                      b * a c * a
                      theorem mul_lt_mul_of_pos_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] (bc : b < c) (a0 : 0 < a) :
                      a * b < a * c
                      theorem mul_lt_mul_of_pos_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosStrictMono α] (bc : b < c) (a0 : 0 < a) :
                      b * a < c * a
                      theorem lt_of_mul_lt_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] (h : a * b < a * c) (a0 : 0 a) :
                      b < c
                      theorem lt_of_mul_lt_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] (h : b * a < c * a) (a0 : 0 a) :
                      b < c
                      theorem le_of_mul_le_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulReflectLE α] (bc : a * b a * c) (a0 : 0 < a) :
                      b c
                      theorem le_of_mul_le_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosReflectLE α] (bc : b * a c * a) (a0 : 0 < a) :
                      b c
                      theorem lt_of_mul_lt_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] (h : a * b < a * c) (a0 : 0 a) :
                      b < c

                      Alias of lt_of_mul_lt_mul_left.

                      theorem lt_of_mul_lt_mul_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] (h : b * a < c * a) (a0 : 0 a) :
                      b < c

                      Alias of lt_of_mul_lt_mul_right.

                      theorem le_of_mul_le_mul_of_pos_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulReflectLE α] (bc : a * b a * c) (a0 : 0 < a) :
                      b c

                      Alias of le_of_mul_le_mul_left.

                      theorem le_of_mul_le_mul_of_pos_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosReflectLE α] (bc : b * a c * a) (a0 : 0 < a) :
                      b c

                      Alias of le_of_mul_le_mul_right.

                      @[simp]
                      theorem mul_lt_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
                      a * b < a * c b < c
                      @[simp]
                      theorem mul_lt_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
                      b * a < c * a b < c
                      @[simp]
                      theorem mul_le_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
                      a * b a * c b c
                      @[simp]
                      theorem mul_le_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) :
                      b * a c * a b c
                      theorem mul_le_mul_iff_of_pos_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
                      a * b a * c b c

                      Alias of mul_le_mul_left.

                      theorem mul_le_mul_iff_of_pos_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) :
                      b * a c * a b c

                      Alias of mul_le_mul_right.

                      theorem mul_lt_mul_iff_of_pos_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
                      a * b < a * c b < c

                      Alias of mul_lt_mul_left.

                      theorem mul_lt_mul_iff_of_pos_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
                      b * a < c * a b < c

                      Alias of mul_lt_mul_right.

                      theorem mul_le_mul_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (h₁ : a b) (h₂ : c d) (a0 : 0 a) (d0 : 0 d) :
                      a * c b * d
                      @[deprecated mul_le_mul_of_nonneg]
                      theorem mul_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (h₁ : a b) (h₂ : c d) (a0 : 0 a) (d0 : 0 d) :
                      a * c b * d

                      Alias of mul_le_mul_of_nonneg.

                      theorem mul_le_mul_of_nonneg' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (h₁ : a b) (h₂ : c d) (c0 : 0 c) (b0 : 0 b) :
                      a * c b * d
                      theorem mul_lt_mul_of_le_of_lt_of_pos_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 d) :
                      a * c < b * d
                      theorem mul_lt_mul_of_pos_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 d) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_le_of_lt_of_pos_of_nonneg.

                      theorem mul_lt_mul_of_le_of_lt_of_nonneg_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a b) (h₂ : c < d) (c0 : 0 c) (b0 : 0 < b) :
                      a * c < b * d
                      theorem mul_lt_mul_of_nonneg_of_pos' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a b) (h₂ : c < d) (c0 : 0 c) (b0 : 0 < b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos.

                      @[deprecated mul_lt_mul_of_le_of_lt_of_nonneg_of_pos]
                      theorem mul_lt_mul_of_le_of_le' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a b) (h₂ : c < d) (c0 : 0 c) (b0 : 0 < b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos.

                      theorem mul_lt_mul_of_lt_of_le_of_nonneg_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c d) (a0 : 0 a) (d0 : 0 < d) :
                      a * c < b * d
                      theorem mul_lt_mul_of_nonneg_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c d) (a0 : 0 a) (d0 : 0 < d) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_lt_of_le_of_nonneg_of_pos.

                      theorem mul_lt_mul_of_lt_of_le_of_pos_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c d) (c0 : 0 < c) (b0 : 0 b) :
                      a * c < b * d
                      theorem mul_lt_mul_of_pos_of_nonneg' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c d) (c0 : 0 < c) (b0 : 0 b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg.

                      @[deprecated mul_lt_mul_of_lt_of_le_of_pos_of_nonneg]
                      theorem mul_lt_mul_of_le_of_lt' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c d) (c0 : 0 < c) (b0 : 0 b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg.

                      theorem mul_lt_mul_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) :
                      a * c < b * d
                      @[deprecated mul_lt_mul_of_pos]
                      theorem mul_lt_mul_of_pos_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_pos.

                      theorem mul_lt_mul_of_pos' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) :
                      a * c < b * d
                      @[deprecated mul_lt_mul_of_pos']
                      theorem mul_lt_mul_of_lt_of_lt' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_pos'.

                      theorem mul_le_mul {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (h₁ : a b) (h₂ : c d) (c0 : 0 c) (b0 : 0 b) :
                      a * c b * d

                      Alias of mul_le_mul_of_nonneg'.

                      theorem mul_lt_mul {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c d) (c0 : 0 < c) (b0 : 0 b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg.


                      Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg.

                      theorem mul_lt_mul' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a b) (h₂ : c < d) (c0 : 0 c) (b0 : 0 < b) :
                      a * c < b * d

                      Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos.


                      Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos.

                      theorem mul_le_of_mul_le_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] (h : a * b c) (hle : d b) (a0 : 0 a) :
                      a * d c
                      theorem mul_lt_of_mul_lt_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] (h : a * b < c) (hle : d b) (a0 : 0 a) :
                      a * d < c
                      theorem le_mul_of_le_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] (h : a b * c) (hle : c d) (b0 : 0 b) :
                      a b * d
                      theorem lt_mul_of_lt_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] (h : a < b * c) (hle : c d) (b0 : 0 b) :
                      a < b * d
                      theorem mul_le_of_mul_le_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] (h : a * b c) (hle : d a) (b0 : 0 b) :
                      d * b c
                      theorem mul_lt_of_mul_lt_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] (h : a * b < c) (hle : d a) (b0 : 0 b) :
                      d * b < c
                      theorem le_mul_of_le_mul_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] (h : a b * c) (hle : b d) (c0 : 0 c) :
                      a d * c
                      theorem lt_mul_of_lt_mul_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] (h : a < b * c) (hle : b d) (c0 : 0 c) :
                      a < d * c
                      @[instance 100]
                      Equations
                      • =
                      @[instance 100]
                      Equations
                      • =
                      theorem Left.mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) :
                      0 < a * b

                      Assumes left covariance.

                      theorem mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) :
                      0 < a * b

                      Alias of Left.mul_pos.


                      Assumes left covariance.

                      theorem mul_neg_of_pos_of_neg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) :
                      a * b < 0
                      @[simp]
                      theorem mul_pos_iff_of_pos_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) :
                      0 < a * b 0 < b
                      theorem Right.mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] (ha : 0 < a) (hb : 0 < b) :
                      0 < a * b

                      Assumes right covariance.

                      theorem mul_neg_of_neg_of_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) :
                      a * b < 0
                      @[simp]
                      theorem mul_pos_iff_of_pos_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) :
                      0 < a * b 0 < a
                      theorem Left.mul_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 a) (hb : 0 b) :
                      0 a * b

                      Assumes left covariance.

                      theorem mul_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 a) (hb : 0 b) :
                      0 a * b

                      Alias of Left.mul_nonneg.


                      Assumes left covariance.

                      theorem mul_nonpos_of_nonneg_of_nonpos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 a) (hb : b 0) :
                      a * b 0
                      theorem Right.mul_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosMono α] (ha : 0 a) (hb : 0 b) :
                      0 a * b

                      Assumes right covariance.

                      theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosMono α] (ha : a 0) (hb : 0 b) :
                      a * b 0
                      theorem pos_of_mul_pos_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulReflectLT α] (h : 0 < a * b) (ha : 0 a) :
                      0 < b
                      theorem pos_of_mul_pos_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosReflectLT α] (h : 0 < a * b) (hb : 0 b) :
                      0 < a
                      theorem pos_iff_pos_of_mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) :
                      0 < a 0 < b
                      theorem Left.mul_lt_mul_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 a) (c0 : 0 c) :
                      a * c < b * d

                      Assumes left strict covariance.

                      theorem Right.mul_lt_mul_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 a) (c0 : 0 c) :
                      a * c < b * d

                      Assumes right strict covariance.

                      theorem mul_lt_mul_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 a) (c0 : 0 c) :
                      a * c < b * d

                      Alias of Left.mul_lt_mul_of_nonneg.


                      Assumes left strict covariance.

                      theorem mul_lt_mul'' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 a) (c0 : 0 c) :
                      a * c < b * d

                      Alias of Left.mul_lt_mul_of_nonneg.


                      Assumes left strict covariance.

                      theorem mul_self_le_mul_self {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (ha : 0 a) (hab : a b) :
                      a * a b * b
                      theorem posMulMono_iff_covariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] :
                      PosMulMono α CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x x_1
                      theorem mulPosMono_iff_covariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] :
                      MulPosMono α CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x x_1
                      theorem posMulReflectLT_iff_contravariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] :
                      PosMulReflectLT α ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x < x_1
                      theorem mulPosReflectLT_iff_contravariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] :
                      MulPosReflectLT α ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x < x_1
                      @[instance 100]
                      Equations
                      • =
                      @[instance 100]
                      Equations
                      • =
                      @[instance 100]
                      Equations
                      • =
                      @[instance 100]
                      Equations
                      • =
                      theorem mul_left_cancel_iff_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulZeroClass α] [PartialOrder α] [PosMulReflectLE α] (a0 : 0 < a) :
                      a * b = a * c b = c
                      theorem mul_right_cancel_iff_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulZeroClass α] [PartialOrder α] [MulPosReflectLE α] (b0 : 0 < b) :
                      a * b = c * b a = c
                      theorem mul_eq_mul_iff_eq_and_eq_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] [MulPosStrictMono α] (hab : a b) (hcd : c d) (a0 : 0 < a) (d0 : 0 < d) :
                      a * c = b * d a = b c = d
                      theorem mul_eq_mul_iff_eq_and_eq_of_pos' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] [MulPosStrictMono α] (hab : a b) (hcd : c d) (b0 : 0 < b) (c0 : 0 < c) :
                      a * c = b * d a = b c = d
                      theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
                      0 < a 0 < b a < 0 b < 0
                      theorem neg_of_mul_pos_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a 0) :
                      b < 0
                      theorem neg_of_mul_pos_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b 0) :
                      a < 0
                      theorem neg_iff_neg_of_mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
                      a < 0 b < 0
                      theorem Left.neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (a0 : 0 a) :
                      b < 0
                      theorem neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (a0 : 0 a) :
                      b < 0

                      Alias of Left.neg_of_mul_neg_right.

                      theorem Right.neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [MulPosMono α] (h : a * b < 0) (a0 : 0 a) :
                      b < 0
                      theorem Left.neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (b0 : 0 b) :
                      a < 0
                      theorem neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (b0 : 0 b) :
                      a < 0

                      Alias of Left.neg_of_mul_neg_left.

                      theorem Right.neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [MulPosMono α] (h : a * b < 0) (b0 : 0 b) :
                      a < 0

                      Lemmas of the form a ≤ a * b ↔ 1 ≤ b and a * b ≤ a ↔ b ≤ 1, which assume left covariance.

                      @[simp]
                      theorem le_mul_iff_one_le_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
                      a a * b 1 b
                      @[simp]
                      theorem lt_mul_iff_one_lt_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
                      a < a * b 1 < b
                      @[simp]
                      theorem mul_le_iff_le_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
                      a * b a b 1
                      @[simp]
                      theorem mul_lt_iff_lt_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
                      a * b < a b < 1

                      Lemmas of the form a ≤ b * a ↔ 1 ≤ b and a * b ≤ b ↔ a ≤ 1, which assume right covariance.

                      @[simp]
                      theorem le_mul_iff_one_le_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) :
                      a b * a 1 b
                      @[simp]
                      theorem lt_mul_iff_one_lt_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
                      a < b * a 1 < b
                      @[simp]
                      theorem mul_le_iff_le_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] [MulPosReflectLE α] (b0 : 0 < b) :
                      a * b b a 1
                      @[simp]
                      theorem mul_lt_iff_lt_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (b0 : 0 < b) :
                      a * b < b a < 1

                      Lemmas of the form 1 ≤ b → a ≤ a * b.

                      Variants with < 0 and ≤ 0 instead of 0 < and 0 ≤ appear in Mathlib/Algebra/Order/Ring/Defs (which imports this file) as they need additional results which are not yet available here.

                      theorem mul_le_of_le_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (hb : 0 b) (h : a 1) :
                      a * b b
                      theorem le_mul_of_one_le_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (hb : 0 b) (h : 1 a) :
                      b a * b
                      theorem mul_le_of_le_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 0 a) (h : b 1) :
                      a * b a
                      theorem le_mul_of_one_le_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 0 a) (h : 1 b) :
                      a a * b
                      theorem mul_lt_of_lt_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) :
                      a * b < b
                      theorem lt_mul_of_one_lt_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) :
                      b < a * b
                      theorem mul_lt_of_lt_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) :
                      a * b < a
                      theorem lt_mul_of_one_lt_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (h : 1 < b) :
                      a < a * b

                      Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c.

                      theorem mul_le_of_le_of_le_one_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : b c) (ha : a 1) (hb : 0 b) :
                      b * a c
                      theorem mul_lt_of_le_of_lt_one_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (bc : b c) (ha : a < 1) (b0 : 0 < b) :
                      b * a < c
                      theorem mul_lt_of_lt_of_le_one_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : b < c) (ha : a 1) (hb : 0 b) :
                      b * a < c
                      theorem Left.mul_le_one_of_le_of_le {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : a 1) (hb : b 1) (a0 : 0 a) :
                      a * b 1

                      Assumes left covariance.

                      theorem Left.mul_lt_of_le_of_lt_one_of_pos {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (ha : a 1) (hb : b < 1) (a0 : 0 < a) :
                      a * b < 1

                      Assumes left covariance.

                      theorem Left.mul_lt_of_lt_of_le_one_of_nonneg {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : a < 1) (hb : b 1) (a0 : 0 a) :
                      a * b < 1

                      Assumes left covariance.

                      theorem mul_le_of_le_of_le_one' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (bc : b c) (ha : a 1) (a0 : 0 a) (c0 : 0 c) :
                      b * a c
                      theorem mul_lt_of_lt_of_le_one' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : a 1) (a0 : 0 < a) (c0 : 0 c) :
                      b * a < c
                      theorem mul_lt_of_le_of_lt_one' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (bc : b c) (ha : a < 1) (a0 : 0 a) (c0 : 0 < c) :
                      b * a < c
                      theorem mul_lt_of_lt_of_lt_one_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : a 1) (a0 : 0 < a) (c0 : 0 c) :
                      b * a < c

                      Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a.

                      theorem le_mul_of_le_of_one_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : b c) (ha : 1 a) (hc : 0 c) :
                      b c * a
                      theorem lt_mul_of_le_of_one_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (bc : b c) (ha : 1 < a) (c0 : 0 < c) :
                      b < c * a
                      theorem lt_mul_of_lt_of_one_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : b < c) (ha : 1 a) (hc : 0 c) :
                      b < c * a
                      theorem Left.one_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 1 a) (hb : 1 b) (a0 : 0 a) :
                      1 a * b

                      Assumes left covariance.

                      theorem Left.one_lt_mul_of_le_of_lt_of_pos {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (ha : 1 a) (hb : 1 < b) (a0 : 0 < a) :
                      1 < a * b

                      Assumes left covariance.

                      theorem Left.lt_mul_of_lt_of_one_le_of_nonneg {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 1 < a) (hb : 1 b) (a0 : 0 a) :
                      1 < a * b

                      Assumes left covariance.

                      theorem le_mul_of_le_of_one_le' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (bc : b c) (ha : 1 a) (a0 : 0 a) (b0 : 0 b) :
                      b c * a
                      theorem lt_mul_of_le_of_one_lt' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (bc : b c) (ha : 1 < a) (a0 : 0 a) (b0 : 0 < b) :
                      b < c * a
                      theorem lt_mul_of_lt_of_one_le' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : 1 a) (a0 : 0 < a) (b0 : 0 b) :
                      b < c * a
                      theorem lt_mul_of_lt_of_one_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (bc : b < c) (ha : 1 < a) (a0 : 0 < a) (b0 : 0 < b) :
                      b < c * a

                      Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c.

                      theorem mul_le_of_le_one_of_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : a 1) (h : b c) (hb : 0 b) :
                      a * b c
                      theorem mul_lt_of_lt_one_of_le_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (ha : a < 1) (h : b c) (hb : 0 < b) :
                      a * b < c
                      theorem mul_lt_of_le_one_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : a 1) (h : b < c) (hb : 0 b) :
                      a * b < c
                      theorem Right.mul_lt_one_of_lt_of_le_of_pos {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (ha : a < 1) (hb : b 1) (b0 : 0 < b) :
                      a * b < 1

                      Assumes right covariance.

                      theorem Right.mul_lt_one_of_le_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : a 1) (hb : b < 1) (b0 : 0 b) :
                      a * b < 1

                      Assumes right covariance.

                      theorem mul_lt_of_lt_one_of_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (ha : a < 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 < c) :
                      a * b < c
                      theorem Right.mul_le_one_of_le_of_le {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : a 1) (hb : b 1) (b0 : 0 b) :
                      a * b 1

                      Assumes right covariance.

                      theorem mul_le_of_le_one_of_le' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (ha : a 1) (bc : b c) (a0 : 0 a) (c0 : 0 c) :
                      a * b c
                      theorem mul_lt_of_lt_one_of_le' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (ha : a < 1) (bc : b c) (a0 : 0 a) (c0 : 0 < c) :
                      a * b < c
                      theorem mul_lt_of_le_one_of_lt' {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (ha : a 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 c) :
                      a * b < c

                      Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c.

                      theorem lt_mul_of_one_lt_of_le_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (ha : 1 < a) (h : b c) (hc : 0 < c) :
                      b < a * c
                      theorem lt_mul_of_one_le_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : 1 a) (h : b < c) (hc : 0 c) :
                      b < a * c
                      theorem lt_mul_of_one_lt_of_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (ha : 1 < a) (h : b < c) (hc : 0 < c) :
                      b < a * c
                      theorem Right.one_lt_mul_of_lt_of_le_of_pos {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (ha : 1 < a) (hb : 1 b) (b0 : 0 < b) :
                      1 < a * b

                      Assumes right covariance.

                      theorem Right.one_lt_mul_of_le_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : 1 a) (hb : 1 < b) (b0 : 0 b) :
                      1 < a * b

                      Assumes right covariance.

                      theorem Right.one_lt_mul_of_lt_of_lt {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (ha : 1 < a) (hb : 1 < b) (b0 : 0 < b) :
                      1 < a * b

                      Assumes right covariance.

                      theorem lt_mul_of_one_lt_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : 1 a) (h : b < c) (hc : 0 c) :
                      b < a * c
                      theorem lt_of_mul_lt_of_one_le_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : a * b < c) (hle : 1 b) (ha : 0 a) :
                      a < c
                      theorem lt_of_lt_mul_of_le_one_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : a < b * c) (hc : c 1) (hb : 0 b) :
                      a < b
                      theorem lt_of_lt_mul_of_le_one_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (h : a < b * c) (hb : b 1) (hc : 0 c) :
                      a < c
                      theorem le_mul_of_one_le_of_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : 1 a) (bc : b c) (c0 : 0 c) :
                      b a * c
                      theorem Right.one_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (ha : 1 a) (hb : 1 b) (b0 : 0 b) :
                      1 a * b

                      Assumes right covariance.

                      theorem le_of_mul_le_of_one_le_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : a * b c) (hb : 1 b) (ha : 0 a) :
                      a c
                      theorem le_of_le_mul_of_le_one_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (h : a b * c) (hc : c 1) (hb : 0 b) :
                      a b
                      theorem le_of_mul_le_of_one_le_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (h : a * b c) (ha : 1 a) (hb : 0 b) :
                      b c
                      theorem le_of_le_mul_of_le_one_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (h : a b * c) (hb : b 1) (hc : 0 c) :
                      a c
                      theorem exists_square_le' {α : Type u_1} {a : α} [MulOneClass α] [Zero α] [LinearOrder α] [PosMulStrictMono α] (a0 : 0 < a) :
                      ∃ (b : α), b * b a
                      theorem posMulStrictMono_iff_mulPosStrictMono {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [Preorder α] :
                      theorem posMulReflectLT_iff_mulPosReflectLT {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [Preorder α] :
                      theorem posMulMono_iff_mulPosMono {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [Preorder α] :
                      theorem posMulReflectLE_iff_mulPosReflectLE {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [Preorder α] :