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).

@[reducible, inline]
abbrev PosMulMono (α : Type u_3) [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_3) [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_3) [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_3) [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_3) [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_3) [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_3) [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_3) [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_3} [Mul α] [Zero α] [Preorder α] [PosMulMono α] :
                  CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x1 x2 : α) => x1 x2
                  instance MulPosMono.to_covariantClass_pos_mul_le {α : Type u_3} [Mul α] [Zero α] [Preorder α] [MulPosMono α] :
                  CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x1 x2 : α) => x1 x2
                  instance PosMulReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_3} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] :
                  ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x1 x2 : α) => x1 < x2
                  instance MulPosReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_3} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] :
                  ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x1 x2 : α) => x1 < x2
                  @[instance 100]
                  instance MulLeftMono.toPosMulMono {α : Type u_3} [Mul α] [Zero α] [Preorder α] [MulLeftMono α] :
                  @[instance 100]
                  instance MulRightMono.toMulPosMono {α : Type u_3} [Mul α] [Zero α] [Preorder α] [MulRightMono α] :
                  @[instance 100]
                  @[instance 100]
                  @[instance 100]
                  @[instance 100]
                  @[instance 100]
                  @[instance 100]
                  theorem mul_le_mul_of_nonneg_left {α : Type u_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {a b c d : α} [Mul α] [Zero α] [Preorder α] [MulPosMono α] (h : a < b * c) (hle : b d) (c0 : 0 c) :
                  a < d * c
                  @[instance 100]
                  @[instance 100]
                  theorem Left.mul_pos {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) :
                  0 < a * b

                  Assumes left covariance.

                  theorem mul_pos {α : Type u_3} {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_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) :
                  a * b < 0
                  @[simp]
                  theorem mul_pos_iff_of_pos_left {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) :
                  0 < a * b 0 < b
                  theorem Right.mul_pos {α : Type u_3} {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_3} {a b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) :
                  a * b < 0
                  @[simp]
                  theorem mul_pos_iff_of_pos_right {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) :
                  0 < a * b 0 < a
                  theorem Left.mul_nonneg {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 a) (hb : 0 b) :
                  0 a * b

                  Assumes left covariance.

                  theorem mul_nonneg {α : Type u_3} {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_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 a) (hb : b 0) :
                  a * b 0
                  theorem Right.mul_nonneg {α : Type u_3} {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_3} {a b : α} [MulZeroClass α] [Preorder α] [MulPosMono α] (ha : a 0) (hb : 0 b) :
                  a * b 0
                  theorem pos_of_mul_pos_right {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulReflectLT α] (h : 0 < a * b) (ha : 0 a) :
                  0 < b
                  theorem pos_of_mul_pos_left {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [MulPosReflectLT α] (h : 0 < a * b) (hb : 0 b) :
                  0 < a
                  theorem pos_iff_pos_of_mul_pos {α : Type u_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) :
                  0 < a 0 < b
                  theorem Left.mul_lt_mul_of_nonneg {α : Type u_3} {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_3} {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_3} {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_3} {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_3} {a b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (ha : 0 a) (hab : a b) :
                  a * a b * b
                  theorem posMulMono_iff_covariant_pos {α : Type u_3} [MulZeroClass α] [PartialOrder α] :
                  PosMulMono α CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x1 x2 : α) => x1 x2
                  theorem mulPosMono_iff_covariant_pos {α : Type u_3} [MulZeroClass α] [PartialOrder α] :
                  MulPosMono α CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x1 x2 : α) => x1 x2
                  theorem posMulReflectLT_iff_contravariant_pos {α : Type u_3} [MulZeroClass α] [PartialOrder α] :
                  PosMulReflectLT α ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x1 x2 : α) => x1 < x2
                  theorem mulPosReflectLT_iff_contravariant_pos {α : Type u_3} [MulZeroClass α] [PartialOrder α] :
                  MulPosReflectLT α ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x1 x2 : α) => x1 < x2
                  @[instance 100]
                  @[instance 100]
                  theorem mul_left_cancel_iff_of_pos {α : Type u_3} {a b c : α} [MulZeroClass α] [PartialOrder α] [PosMulReflectLE α] (a0 : 0 < a) :
                  a * b = a * c b = c
                  theorem mul_right_cancel_iff_of_pos {α : Type u_3} {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_3} {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_3} {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_3} {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_3} {a b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a 0) :
                  b < 0
                  theorem neg_of_mul_pos_left {α : Type u_3} {a b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b 0) :
                  a < 0
                  theorem neg_iff_neg_of_mul_pos {α : Type u_3} {a b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
                  a < 0 b < 0
                  theorem Left.neg_of_mul_neg_right {α : Type u_3} {a b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (a0 : 0 a) :
                  b < 0
                  theorem neg_of_mul_neg_right {α : Type u_3} {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_3} {a b : α} [MulZeroClass α] [LinearOrder α] [MulPosMono α] (h : a * b < 0) (a0 : 0 a) :
                  b < 0
                  theorem Left.neg_of_mul_neg_left {α : Type u_3} {a b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (b0 : 0 b) :
                  a < 0
                  theorem neg_of_mul_neg_left {α : Type u_3} {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_3} {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.

                  theorem one_lt_of_lt_mul_left₀ {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulReflectLT α] (ha : 0 a) (h : a < a * b) :
                  1 < b
                  theorem one_lt_of_lt_mul_right₀ {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosReflectLT α] (hb : 0 b) (h : b < a * b) :
                  1 < a
                  theorem one_le_of_le_mul_left₀ {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulReflectLE α] (ha : 0 < a) (h : a a * b) :
                  1 b
                  theorem one_le_of_le_mul_right₀ {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosReflectLE α] (hb : 0 < b) (h : b a * b) :
                  1 a
                  @[simp]
                  theorem le_mul_iff_one_le_right {α : Type u_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (hb : 0 b) (h : a 1) :
                  a * b b
                  theorem le_mul_of_one_le_left {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (hb : 0 b) (h : 1 a) :
                  b a * b
                  theorem mul_le_of_le_one_right {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 0 a) (h : b 1) :
                  a * b a
                  theorem le_mul_of_one_le_right {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 0 a) (h : 1 b) :
                  a a * b
                  theorem mul_lt_of_lt_one_left {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) :
                  a * b < b
                  theorem lt_mul_of_one_lt_left {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) :
                  b < a * b
                  theorem mul_lt_of_lt_one_right {α : Type u_3} {a b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) :
                  a * b < a
                  theorem lt_mul_of_one_lt_right {α : Type u_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {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_3} {a : α} [MulOneClass α] [Zero α] [LinearOrder α] [PosMulStrictMono α] (a0 : 0 < a) :
                  ∃ (b : α), b * b a
                  @[simp]
                  theorem pow_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 0 a) (n : ) :
                  0 a ^ n
                  theorem zero_pow_le_one {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] [ZeroLEOneClass M₀] (n : ) :
                  0 ^ n 1
                  theorem pow_le_pow_of_le_one {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha₀ : 0 a) (ha₁ : a 1) {m n : } :
                  m na ^ n a ^ m
                  theorem pow_le_of_le_one {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h₀ : 0 a) (h₁ : a 1) (hn : n 0) :
                  a ^ n a
                  theorem sq_le {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h₀ : 0 a) (h₁ : a 1) :
                  a ^ 2 a
                  theorem one_le_mul_of_one_le_of_one_le {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 a) (hb : 1 b) :
                  1 a * b
                  theorem one_lt_mul_of_le_of_lt {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 a) (hb : 1 < b) :
                  1 < a * b
                  theorem one_lt_mul_of_lt_of_le {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) (hb : 1 b) :
                  1 < a * b
                  theorem one_lt_mul {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 a) (hb : 1 < b) :
                  1 < a * b

                  Alias of one_lt_mul_of_le_of_lt.

                  theorem mul_lt_one_of_nonneg_of_lt_one_left {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [PosMulMono M₀] (ha₀ : 0 a) (ha : a < 1) (hb : b 1) :
                  a * b < 1
                  theorem mul_lt_one_of_nonneg_of_lt_one_right {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [MulPosMono M₀] (ha : a 1) (hb₀ : 0 b) (hb : b < 1) :
                  a * b < 1
                  theorem Bound.one_lt_mul {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] :
                  1 a 1 < b 1 < a 1 b1 < a * b
                  theorem mul_le_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : a 1) (hb₀ : 0 b) (hb : b 1) :
                  a * b 1
                  theorem pow_le_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] {n : } :
                  0 aa 1a ^ n 1
                  theorem pow_lt_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h₀ : 0 a) (h₁ : a < 1) {n : } :
                  n 0a ^ n < 1
                  theorem one_le_pow₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) {n : } :
                  1 a ^ n
                  theorem one_lt_pow₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 < a) {n : } :
                  n 01 < a ^ n
                  theorem pow_right_mono₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h : 1 a) :
                  Monotone fun (x : ) => a ^ x
                  theorem Bound.pow_le_pow_right_of_le_one_or_one_le {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h : 1 a n m 0 a a 1 m n) :
                  a ^ n a ^ m

                  bound lemma for branching on 1 ≤ a ∨ a ≤ 1 when proving a ^ n ≤ a ^ m

                  theorem pow_le_pow_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) (hmn : m n) :
                  a ^ m a ^ n
                  theorem le_self_pow₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) (hn : n 0) :
                  a a ^ n
                  theorem Bound.le_self_pow_of_pos {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) (hn : 0 < n) :
                  a a ^ n

                  The bound tactic can't handle m ≠ 0 goals yet, so we express as 0 < m

                  theorem pow_le_pow_left₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 0 a) (hab : a b) (n : ) :
                  a ^ n b ^ n
                  theorem pow_left_monotoneOn {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] :
                  MonotoneOn (fun (a : M₀) => a ^ n) {x : M₀ | 0 x}
                  theorem monotone_mul_left_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (ha : 0 a) :
                  Monotone fun (x : M₀) => a * x
                  theorem monotone_mul_right_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [MulPosMono M₀] (ha : 0 a) :
                  Monotone fun (x : M₀) => x * a
                  theorem Monotone.mul_const {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : αM₀} [MulPosMono M₀] (hf : Monotone f) (ha : 0 a) :
                  Monotone fun (x : α) => f x * a
                  theorem Monotone.const_mul {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : αM₀} [PosMulMono M₀] (hf : Monotone f) (ha : 0 a) :
                  Monotone fun (x : α) => a * f x
                  theorem Antitone.mul_const {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : αM₀} [MulPosMono M₀] (hf : Antitone f) (ha : 0 a) :
                  Antitone fun (x : α) => f x * a
                  theorem Antitone.const_mul {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : αM₀} [PosMulMono M₀] (hf : Antitone f) (ha : 0 a) :
                  Antitone fun (x : α) => a * f x
                  theorem Monotone.mul {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [Preorder M₀] [Preorder α] {f g : αM₀} [PosMulMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : Monotone g) (hf₀ : ∀ (x : α), 0 f x) (hg₀ : ∀ (x : α), 0 g x) :
                  Monotone (f * g)
                  theorem mul_self_lt_mul_self {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀] [MulPosMono M₀] (ha : 0 a) (hab : a < b) :
                  a * a < b * b
                  theorem strictMonoOn_mul_self {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] [PosMulStrictMono M₀] [MulPosMono M₀] :
                  StrictMonoOn (fun (x : M₀) => x * x) {x : M₀ | 0 x}
                  theorem Decidable.mul_lt_mul'' {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a b c d : M₀} [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] [DecidableRel fun (x1 x2 : M₀) => x1 x2] (h1 : a < c) (h2 : b < d) (h3 : 0 a) (h4 : 0 b) :
                  a * b < c * d
                  theorem lt_mul_left {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [MulPosStrictMono M₀] (ha : 0 < a) (hb : 1 < b) :
                  a < b * a
                  theorem lt_mul_right {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) :
                  a < a * b
                  theorem lt_mul_self {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) :
                  a < a * a
                  @[simp]
                  theorem pow_pos {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulStrictMono M₀] (ha : 0 < a) (n : ) :
                  0 < a ^ n
                  theorem sq_pos_of_pos {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulStrictMono M₀] (ha : 0 < a) :
                  0 < a ^ 2
                  theorem pow_lt_pow_left₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hab : a < b) (ha : 0 a) {n : } :
                  n 0a ^ n < b ^ n
                  theorem pow_left_strictMonoOn₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hn : n 0) :
                  StrictMonoOn (fun (x : M₀) => x ^ n) {a : M₀ | 0 a}

                  See also pow_left_strictMono₀ and Nat.pow_left_strictMono.

                  theorem pow_right_strictMono₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h : 1 < a) :
                  StrictMono fun (x : ) => a ^ x

                  See also pow_right_strictMono'.

                  theorem pow_lt_pow_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h : 1 < a) (hmn : m < n) :
                  a ^ m < a ^ n
                  theorem pow_lt_pow_iff_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h : 1 < a) :
                  a ^ n < a ^ m n < m
                  theorem pow_le_pow_iff_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h : 1 < a) :
                  a ^ n a ^ m n m
                  theorem lt_self_pow₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h : 1 < a) (hm : 1 < m) :
                  a < a ^ m
                  theorem pow_right_strictAnti₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) :
                  StrictAnti fun (x : ) => a ^ x
                  theorem pow_lt_pow_iff_right_of_lt_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) :
                  a ^ m < a ^ n n < m
                  theorem pow_lt_pow_right_of_lt_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) :
                  a ^ n < a ^ m
                  theorem pow_lt_self_of_lt_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {n : } [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) :
                  a ^ n < a
                  theorem strictMono_mul_left_of_pos {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] (ha : 0 < a) :
                  StrictMono fun (x : M₀) => a * x
                  theorem strictMono_mul_right_of_pos {M₀ : Type u_1} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [MulPosStrictMono M₀] (ha : 0 < a) :
                  StrictMono fun (x : M₀) => x * a
                  theorem StrictMono.mul_const {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : αM₀} [MulPosStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) :
                  StrictMono fun (x : α) => f x * a
                  theorem StrictMono.const_mul {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : αM₀} [PosMulStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) :
                  StrictMono fun (x : α) => a * f x
                  theorem StrictAnti.mul_const {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : αM₀} [MulPosStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) :
                  StrictAnti fun (x : α) => f x * a
                  theorem StrictAnti.const_mul {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : αM₀} [PosMulStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) :
                  StrictAnti fun (x : α) => a * f x
                  theorem StrictMono.mul_monotone {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] [Preorder α] {f g : αM₀} [PosMulMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : Monotone g) (hf₀ : ∀ (x : α), 0 f x) (hg₀ : ∀ (x : α), 0 < g x) :
                  theorem Monotone.mul_strictMono {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] [Preorder α] {f g : αM₀} [PosMulStrictMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : StrictMono g) (hf₀ : ∀ (x : α), 0 < f x) (hg₀ : ∀ (x : α), 0 g x) :
                  theorem StrictMono.mul {M₀ : Type u_1} {α : Type u_3} [MonoidWithZero M₀] [PartialOrder M₀] [Preorder α] {f g : αM₀} [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : StrictMono g) (hf₀ : ∀ (x : α), 0 f x) (hg₀ : ∀ (x : α), 0 g x) :
                  theorem pow_le_pow_iff_left₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} {n : } (ha : 0 a) (hb : 0 b) (hn : n 0) :
                  a ^ n b ^ n a b
                  theorem pow_lt_pow_iff_left₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} {n : } (ha : 0 a) (hb : 0 b) (hn : n 0) :
                  a ^ n < b ^ n a < b
                  @[simp]
                  theorem pow_left_inj₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} {n : } (ha : 0 a) (hb : 0 b) (hn : n 0) :
                  a ^ n = b ^ n a = b
                  theorem pow_right_injective₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} (ha₀ : 0 < a) (ha₁ : a 1) :
                  Function.Injective fun (x : ) => a ^ x
                  @[simp]
                  theorem pow_right_inj₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} {m n : } (ha₀ : 0 < a) (ha₁ : a 1) :
                  a ^ m = a ^ n m = n
                  theorem pow_le_one_iff_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} {n : } (ha : 0 a) (hn : n 0) :
                  a ^ n 1 a 1
                  theorem one_le_pow_iff_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} {n : } (ha : 0 a) (hn : n 0) :
                  1 a ^ n 1 a
                  theorem pow_lt_one_iff_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} {n : } (ha : 0 a) (hn : n 0) :
                  a ^ n < 1 a < 1
                  theorem one_lt_pow_iff_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} {n : } (ha : 0 a) (hn : n 0) :
                  1 < a ^ n 1 < a
                  theorem pow_eq_one_iff_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} {n : } (ha : 0 a) (hn : n 0) :
                  a ^ n = 1 a = 1
                  theorem sq_le_one_iff₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} (ha : 0 a) :
                  a ^ 2 1 a 1
                  theorem sq_lt_one_iff₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} (ha : 0 a) :
                  a ^ 2 < 1 a < 1
                  theorem one_le_sq_iff₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} (ha : 0 a) :
                  1 a ^ 2 1 a
                  theorem one_lt_sq_iff₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a : M₀} (ha : 0 a) :
                  1 < a ^ 2 1 < a
                  theorem lt_of_pow_lt_pow_left₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} (n : ) (hb : 0 b) (h : a ^ n < b ^ n) :
                  a < b
                  theorem le_of_pow_le_pow_left₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} {n : } (hn : n 0) (hb : 0 b) (h : a ^ n b ^ n) :
                  a b
                  @[simp]
                  theorem sq_eq_sq₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} (ha : 0 a) (hb : 0 b) :
                  a ^ 2 = b ^ 2 a = b
                  theorem lt_of_mul_self_lt_mul_self₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} (hb : 0 b) :
                  a * a < b * ba < b
                  theorem sq_lt_sq₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} (ha : 0 a) (hb : 0 b) :
                  a ^ 2 < b ^ 2 a < b
                  theorem sq_le_sq₀ {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀} (ha : 0 a) (hb : 0 b) :
                  a ^ 2 b ^ 2 a b
                  theorem div_self_le_one {G₀ : Type u_2} [GroupWithZero G₀] [Preorder G₀] [ZeroLEOneClass G₀] (a : G₀) :
                  a / a 1

                  See div_self for the version with equality when a ≠ 0.

                  @[simp]
                  theorem inv_pos {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} :
                  0 < a⁻¹ 0 < a
                  theorem inv_pos_of_pos {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} :
                  0 < a0 < a⁻¹

                  Alias of the reverse direction of inv_pos.

                  @[simp]
                  theorem inv_nonneg {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} :
                  0 a⁻¹ 0 a
                  theorem inv_nonneg_of_nonneg {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} :
                  0 a0 a⁻¹

                  Alias of the reverse direction of inv_nonneg.

                  theorem one_div_pos {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} :
                  0 < 1 / a 0 < a
                  theorem one_div_nonneg {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} :
                  0 1 / a 0 a
                  theorem div_pos {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulStrictMono G₀] (ha : 0 < a) (hb : 0 < b) :
                  0 < a / b
                  theorem div_nonneg {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulMono G₀] (ha : 0 a) (hb : 0 b) :
                  0 a / b
                  theorem div_nonpos_of_nonpos_of_nonneg {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] (ha : a 0) (hb : 0 b) :
                  a / b 0
                  theorem zpow_nonneg {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha : 0 a) (n : ) :
                  0 a ^ n
                  theorem zpow_pos {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha : 0 < a) (n : ) :
                  0 < a ^ n
                  @[deprecated zpow_pos]
                  theorem zpow_pos_of_pos {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha : 0 < a) (n : ) :
                  0 < a ^ n

                  Alias of zpow_pos.

                  theorem le_inv_mul_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [PosMulMono G₀] (hc : 0 < c) :
                  a c⁻¹ * b c * a b

                  See le_inv_mul_iff₀' for a version with multiplication on the other side.

                  theorem inv_mul_le_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [PosMulMono G₀] (hc : 0 < c) :
                  c⁻¹ * b a b c * a

                  See inv_mul_le_iff₀' for a version with multiplication on the other side.

                  theorem one_le_inv_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulMono G₀] (ha : 0 < a) :
                  1 a⁻¹ * b a b
                  theorem inv_mul_le_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulMono G₀] (ha : 0 < a) :
                  a⁻¹ * b 1 b a
                  theorem inv_le_iff_one_le_mul₀' {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulMono G₀] (ha : 0 < a) :
                  a⁻¹ b 1 a * b

                  See inv_le_iff_one_le_mul₀ for a version with multiplication on the other side.

                  theorem one_le_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha : 0 < a) :
                  1 a⁻¹ a 1
                  theorem inv_le_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha : 0 < a) :
                  a⁻¹ 1 1 a
                  theorem Bound.one_le_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha : 0 < a) :
                  a 11 a⁻¹

                  Alias of the reverse direction of one_le_inv₀.

                  theorem inv_le_one_of_one_le₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha : 1 a) :
                  theorem one_le_inv_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] :
                  1 a⁻¹ 0 < a a 1
                  theorem mul_le_of_le_inv_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [PosMulMono G₀] (hb : 0 b) (hc : 0 c) (h : a c⁻¹ * b) :
                  c * a b

                  One direction of le_inv_mul_iff₀ where c is allowed to be 0 (but b must be nonnegative).

                  theorem inv_mul_le_of_le_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [PosMulMono G₀] (hb : 0 b) (hc : 0 c) (h : a b * c) :
                  b⁻¹ * a c

                  One direction of inv_mul_le_iff₀ where b is allowed to be 0 (but c must be nonnegative).

                  theorem inv_mul_le_one_of_le₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulMono G₀] (h : a b) (hb : 0 b) :
                  b⁻¹ * a 1
                  theorem zpow_right_mono₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha : 1 a) :
                  Monotone fun (n : ) => a ^ n
                  theorem zpow_right_anti₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] (ha₀ : 0 < a) (ha₁ : a 1) :
                  Antitone fun (n : ) => a ^ n
                  theorem zpow_le_zpow_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] {m n : } (ha : 1 a) (hmn : m n) :
                  a ^ m a ^ n
                  theorem zpow_le_zpow_right_of_le_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] {m n : } (ha₀ : 0 < a) (ha₁ : a 1) (hmn : m n) :
                  a ^ n a ^ m
                  theorem one_le_zpow₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] {n : } (ha : 1 a) (hn : 0 n) :
                  1 a ^ n
                  theorem zpow_le_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a 1) (hn : 0 n) :
                  a ^ n 1
                  theorem zpow_le_one_of_nonpos₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] {n : } (ha : 1 a) (hn : n 0) :
                  a ^ n 1
                  theorem one_le_zpow_of_nonpos₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a 1) (hn : n 0) :
                  1 a ^ n
                  theorem le_mul_inv_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hc : 0 < c) :
                  a b * c⁻¹ a * c b

                  See le_mul_inv_iff₀' for a version with multiplication on the other side.

                  theorem mul_inv_le_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hc : 0 < c) :
                  b * c⁻¹ a b a * c

                  See mul_inv_le_iff₀' for a version with multiplication on the other side.

                  theorem le_div_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hc : 0 < c) :
                  a b / c a * c b

                  See le_div_iff₀' for a version with multiplication on the other side.

                  theorem div_le_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hc : 0 < c) :
                  b / c a b a * c

                  See div_le_iff₀' for a version with multiplication on the other side.

                  theorem inv_le_iff_one_le_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] (ha : 0 < a) :
                  a⁻¹ b 1 b * a

                  See inv_le_iff_one_le_mul₀' for a version with multiplication on the other side.

                  theorem one_le_div₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] (hb : 0 < b) :
                  1 a / b b a
                  theorem div_le_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] (hb : 0 < b) :
                  a / b 1 a b
                  theorem mul_le_of_le_mul_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hb : 0 b) (hc : 0 c) (h : a b * c⁻¹) :
                  a * c b

                  One direction of le_mul_inv_iff₀ where c is allowed to be 0 (but b must be nonnegative).

                  theorem mul_inv_le_of_le_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hb : 0 b) (hc : 0 c) (h : a c * b) :
                  a * b⁻¹ c

                  One direction of mul_inv_le_iff₀ where b is allowed to be 0 (but c must be nonnegative).

                  theorem mul_le_of_le_div₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hb : 0 b) (hc : 0 c) (h : a b / c) :
                  a * c b

                  One direction of le_div_iff₀ where c is allowed to be 0 (but b must be nonnegative).

                  theorem div_le_of_le_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hb : 0 b) (hc : 0 c) (h : a c * b) :
                  a / b c

                  One direction of div_le_iff₀ where b is allowed to be 0 (but c must be nonnegative).

                  theorem mul_inv_le_one_of_le₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] (h : a b) (hb : 0 b) :
                  a * b⁻¹ 1
                  theorem div_le_one_of_le₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] (h : a b) (hb : 0 b) :
                  a / b 1
                  theorem div_le_div_of_nonneg_right {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hab : a b) (hc : 0 c) :
                  a / c b / c
                  @[deprecated le_div_iff₀]
                  theorem le_div_iff {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hc : 0 < c) :
                  a b / c a * c b

                  Alias of le_div_iff₀.


                  See le_div_iff₀' for a version with multiplication on the other side.

                  @[deprecated div_le_iff₀]
                  theorem div_le_iff {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] (hc : 0 < c) :
                  b / c a b a * c

                  Alias of div_le_iff₀.


                  See div_le_iff₀' for a version with multiplication on the other side.

                  theorem inv_le_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] [PosMulMono G₀] (ha : 0 < a) (hb : 0 < b) :

                  See inv_anti₀ for the implication from right-to-left with one fewer assumption.

                  theorem inv_anti₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] [PosMulMono G₀] (hb : 0 < b) (hba : b a) :
                  theorem inv_le_comm₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] [PosMulMono G₀] (ha : 0 < a) (hb : 0 < b) :

                  See also inv_le_of_inv_le₀ for a one-sided implication with one fewer assumption.

                  theorem inv_le_of_inv_le₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] [PosMulMono G₀] (ha : 0 < a) (h : a⁻¹ b) :
                  theorem le_inv_comm₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] [PosMulMono G₀] (ha : 0 < a) (hb : 0 < b) :

                  See also le_inv_of_le_inv₀ for a one-sided implication with one fewer assumption.

                  theorem le_inv_of_le_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] [PosMulMono G₀] (ha : 0 < a) (h : a b⁻¹) :
                  theorem div_le_div_of_nonneg_left {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosMono G₀] [PosMulMono G₀] (ha : 0 a) (hc : 0 < c) (h : c b) :
                  a / b a / c
                  theorem lt_inv_mul_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [PosMulStrictMono G₀] (hc : 0 < c) :
                  a < c⁻¹ * b c * a < b

                  See lt_inv_mul_iff₀' for a version with multiplication on the other side.

                  theorem inv_mul_lt_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [PosMulStrictMono G₀] (hc : 0 < c) :
                  c⁻¹ * b < a b < c * a

                  See inv_mul_lt_iff₀' for a version with multiplication on the other side.

                  theorem inv_lt_iff_one_lt_mul₀' {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulStrictMono G₀] (ha : 0 < a) :
                  a⁻¹ < b 1 < a * b

                  See inv_lt_iff_one_lt_mul₀ for a version with multiplication on the other side.

                  theorem one_lt_inv_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulStrictMono G₀] (ha : 0 < a) :
                  1 < a⁻¹ * b a < b
                  theorem inv_mul_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [PosMulStrictMono G₀] (ha : 0 < a) :
                  a⁻¹ * b < 1 b < a
                  theorem one_lt_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha : 0 < a) :
                  1 < a⁻¹ a < 1
                  theorem inv_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha : 0 < a) :
                  a⁻¹ < 1 1 < a
                  theorem inv_lt_one_of_one_lt₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha : 1 < a) :
                  a⁻¹ < 1
                  theorem one_lt_inv_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] :
                  1 < a⁻¹ 0 < a a < 1
                  theorem zpow_right_strictMono₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha : 1 < a) :
                  StrictMono fun (n : ) => a ^ n
                  theorem zpow_right_strictAnti₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] (ha₀ : 0 < a) (ha₁ : a < 1) :
                  StrictAnti fun (n : ) => a ^ n
                  theorem zpow_lt_zpow_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha : 1 < a) (hmn : m < n) :
                  a ^ m < a ^ n
                  theorem zpow_lt_zpow_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha₀ : 0 < a) (ha₁ : a < 1) (hmn : m < n) :
                  a ^ n < a ^ m
                  theorem one_lt_zpow₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha : 1 < a) (hn : 0 < n) :
                  1 < a ^ n
                  theorem zpow_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a < 1) (hn : 0 < n) :
                  a ^ n < 1
                  theorem zpow_lt_one_of_neg₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha : 1 < a) (hn : n < 0) :
                  a ^ n < 1
                  theorem one_lt_zpow_of_neg₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a < 1) (hn : n < 0) :
                  1 < a ^ n
                  @[simp]
                  theorem zpow_le_zpow_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha : 1 < a) :
                  a ^ m a ^ n m n
                  @[simp]
                  theorem zpow_lt_zpow_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha : 1 < a) :
                  a ^ m < a ^ n m < n
                  theorem zpow_le_zpow_iff_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha₀ : 0 < a) (ha₁ : a < 1) :
                  a ^ m a ^ n n m
                  theorem zpow_lt_zpow_iff_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha₀ : 0 < a) (ha₁ : a < 1) :
                  a ^ m < a ^ n n < m
                  @[simp]
                  theorem one_le_zpow_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha : 1 < a) :
                  1 a ^ n 0 n
                  @[simp]
                  theorem one_lt_zpow_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha : 1 < a) :
                  1 < a ^ n 0 < n
                  @[simp]
                  theorem one_le_zpow_iff_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a < 1) :
                  1 a ^ n n 0
                  @[simp]
                  theorem one_lt_zpow_iff_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a < 1) :
                  1 < a ^ n n < 0
                  @[simp]
                  theorem zpow_le_one_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha : 1 < a) :
                  a ^ n 1 n 0
                  @[simp]
                  theorem zpow_lt_one_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha : 1 < a) :
                  a ^ n < 1 n < 0
                  @[simp]
                  theorem zpow_le_one_iff_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a < 1) :
                  a ^ n 1 0 n
                  @[simp]
                  theorem zpow_lt_one_iff_right_of_lt_one₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀] {n : } (ha₀ : 0 < a) (ha₁ : a < 1) :
                  a ^ n < 1 0 < n
                  theorem lt_mul_inv_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosStrictMono G₀] (hc : 0 < c) :
                  a < b * c⁻¹ a * c < b

                  See lt_mul_inv_iff₀' for a version with multiplication on the other side.

                  theorem mul_inv_lt_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosStrictMono G₀] (hc : 0 < c) :
                  b * c⁻¹ < a b < a * c

                  See mul_inv_lt_iff₀' for a version with multiplication on the other side.

                  theorem lt_div_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosStrictMono G₀] (hc : 0 < c) :
                  a < b / c a * c < b

                  See lt_div_iff₀' for a version with multiplication on the other side.

                  theorem div_lt_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosStrictMono G₀] (hc : 0 < c) :
                  b / c < a b < a * c

                  See div_lt_iff₀' for a version with multiplication on the other side.

                  theorem inv_lt_iff_one_lt_mul₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] (ha : 0 < a) :
                  a⁻¹ < b 1 < b * a

                  See inv_lt_iff_one_lt_mul₀' for a version with multiplication on the other side.

                  theorem div_lt_div_of_pos_right {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosStrictMono G₀] (h : a < b) (hc : 0 < c) :
                  a / c < b / c
                  theorem inv_lt_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (ha : 0 < a) (hb : 0 < b) :
                  a⁻¹ < b⁻¹ b < a

                  See inv_strictAnti₀ for the implication from right-to-left with one fewer assumption.

                  theorem inv_strictAnti₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (hb : 0 < b) (hba : b < a) :
                  theorem inv_lt_comm₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (ha : 0 < a) (hb : 0 < b) :
                  a⁻¹ < b b⁻¹ < a

                  See also inv_lt_of_inv_lt₀ for a one-sided implication with one fewer assumption.

                  theorem inv_lt_of_inv_lt₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (ha : 0 < a) (h : a⁻¹ < b) :
                  b⁻¹ < a
                  theorem lt_inv_comm₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (ha : 0 < a) (hb : 0 < b) :
                  a < b⁻¹ b < a⁻¹

                  See also lt_inv_of_lt_inv₀ for a one-sided implication with one fewer assumption.

                  theorem lt_inv_of_lt_inv₀ {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (ha : 0 < a) (h : a < b⁻¹) :
                  b < a⁻¹
                  theorem div_lt_div_of_pos_left {G₀ : Type u_2} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} [MulPosStrictMono G₀] [PosMulStrictMono G₀] (ha : 0 < a) (hc : 0 < c) (h : c < b) :
                  a / b < a / c
                  @[simp]
                  theorem inv_neg'' {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulMono G₀] :
                  a⁻¹ < 0 a < 0
                  @[simp]
                  theorem inv_nonpos {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulMono G₀] :
                  a⁻¹ 0 a 0
                  theorem inv_lt_zero {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulMono G₀] :
                  a⁻¹ < 0 a < 0

                  Alias of inv_neg''.

                  theorem one_div_neg {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulMono G₀] :
                  1 / a < 0 a < 0
                  theorem one_div_nonpos {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulMono G₀] :
                  1 / a 0 a 0
                  theorem div_nonpos_of_nonneg_of_nonpos {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b : G₀} [PosMulMono G₀] (ha : 0 a) (hb : b 0) :
                  a / b 0
                  theorem neg_of_div_neg_right {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b : G₀} [PosMulMono G₀] (h : a / b < 0) (ha : 0 a) :
                  b < 0
                  theorem neg_of_div_neg_left {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b : G₀} [PosMulMono G₀] (h : a / b < 0) (hb : 0 b) :
                  a < 0
                  theorem inv_lt_one_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulStrictMono G₀] :
                  a⁻¹ < 1 a 0 1 < a
                  theorem inv_le_one_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulStrictMono G₀] :
                  a⁻¹ 1 a 0 1 a
                  theorem zpow_right_injective₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulStrictMono G₀] (ha₀ : 0 < a) (ha₁ : a 1) :
                  Function.Injective fun (n : ) => a ^ n
                  @[simp]
                  theorem zpow_right_inj₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulStrictMono G₀] {m n : } (ha₀ : 0 < a) (ha₁ : a 1) :
                  a ^ m = a ^ n m = n
                  theorem zpow_eq_one_iff_right₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a : G₀} [PosMulStrictMono G₀] (ha₀ : 0 a) (ha₁ : a 1) {n : } :
                  a ^ n = 1 n = 0
                  theorem div_le_div_iff_of_pos_right {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (hc : 0 < c) :
                  a / c b / c a b
                  theorem div_lt_div_iff_of_pos_right {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (hc : 0 < c) :
                  a / c < b / c a < b
                  theorem div_lt_div_iff_of_pos_left {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
                  a / b < a / c c < b
                  theorem div_le_div_iff_of_pos_left {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
                  a / b a / c c b
                  theorem div_le_div₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c d : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (hc : 0 c) (hac : a c) (hd : 0 < d) (hdb : d b) :
                  a / b c / d
                  theorem div_lt_div₀ {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c d : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (hac : a < c) (hdb : d b) (hc : 0 c) (hd : 0 < d) :
                  a / b < c / d
                  theorem div_lt_div₀' {G₀ : Type u_2} [GroupWithZero G₀] [LinearOrder G₀] [ZeroLEOneClass G₀] {a b c d : G₀} [PosMulStrictMono G₀] [MulPosStrictMono G₀] (hac : a c) (hdb : d < b) (hc : 0 < c) (hd : 0 < d) :
                  a / b < c / d
                  theorem posMulStrictMono_iff_mulPosStrictMono {α : Type u_3} [Mul α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [Zero α] [Preorder α] :
                  theorem posMulReflectLT_iff_mulPosReflectLT {α : Type u_3} [Mul α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [Zero α] [Preorder α] :
                  theorem posMulMono_iff_mulPosMono {α : Type u_3} [Mul α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [Zero α] [Preorder α] :
                  theorem posMulReflectLE_iff_mulPosReflectLE {α : Type u_3} [Mul α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [Zero α] [Preorder α] :
                  theorem le_inv_mul_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a c⁻¹ * b c * a b

                  See le_inv_mul_iff₀ for a version with multiplication on the other side.

                  theorem inv_mul_le_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  c⁻¹ * b a b a * c

                  See inv_mul_le_iff₀ for a version with multiplication on the other side.

                  theorem le_mul_inv_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a b * c⁻¹ c * a b

                  See le_mul_inv_iff₀ for a version with multiplication on the other side.

                  theorem mul_inv_le_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  b * c⁻¹ a b c * a

                  See mul_inv_le_iff₀ for a version with multiplication on the other side.

                  theorem div_le_div_iff₀ {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c d : G₀} (hb : 0 < b) (hd : 0 < d) :
                  a / b c / d a * d c * b
                  theorem le_div_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a b / c c * a b

                  See le_div_iff₀ for a version with multiplication on the other side.

                  theorem div_le_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  b / c a b c * a

                  See div_le_iff₀ for a version with multiplication on the other side.

                  theorem le_div_comm₀ {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (ha : 0 < a) (hc : 0 < c) :
                  a b / c c b / a
                  theorem div_le_comm₀ {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hb : 0 < b) (hc : 0 < c) :
                  a / b c a / c b
                  @[deprecated le_div_iff₀']
                  theorem le_div_iff' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a b / c c * a b

                  Alias of le_div_iff₀'.


                  See le_div_iff₀ for a version with multiplication on the other side.

                  @[deprecated div_le_iff₀']
                  theorem div_le_iff' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulMono G₀] {a b c : G₀} (hc : 0 < c) :
                  b / c a b c * a

                  Alias of div_le_iff₀'.


                  See div_le_iff₀ for a version with multiplication on the other side.

                  theorem lt_inv_mul_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a < c⁻¹ * b a * c < b

                  See lt_inv_mul_iff₀ for a version with multiplication on the other side.

                  theorem inv_mul_lt_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hc : 0 < c) :
                  c⁻¹ * b < a b < a * c

                  See inv_mul_lt_iff₀ for a version with multiplication on the other side.

                  theorem lt_mul_inv_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a < b * c⁻¹ c * a < b

                  See lt_mul_inv_iff₀ for a version with multiplication on the other side.

                  theorem mul_inv_lt_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hc : 0 < c) :
                  b * c⁻¹ < a b < c * a

                  See mul_inv_lt_iff₀ for a version with multiplication on the other side.

                  theorem div_lt_div_iff₀ {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c d : G₀} (hb : 0 < b) (hd : 0 < d) :
                  a / b < c / d a * d < c * b
                  theorem lt_div_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hc : 0 < c) :
                  a < b / c c * a < b

                  See lt_div_iff₀ for a version with multiplication on the other side.

                  theorem div_lt_iff₀' {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hc : 0 < c) :
                  b / c < a b < c * a

                  See div_lt_iff₀ for a version with multiplication on the other side.

                  theorem lt_div_comm₀ {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (ha : 0 < a) (hc : 0 < c) :
                  a < b / c c < b / a
                  theorem div_lt_comm₀ {G₀ : Type u_2} [CommGroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [PosMulStrictMono G₀] {a b c : G₀} (hb : 0 < b) (hc : 0 < c) :
                  a / b < c a / c < b