Documentation

Mathlib.Algebra.Order.Module.Defs

Monotonicity of scalar 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, OrderedSMul 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, α and β are orders which have a 0 and such that α acts on β by scalar 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 scalar multiplication (b ↦ a • b):

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

Constructors #

The four typeclasses about nonnegativity can usually be checked only on positive inputs due to their condition becoming trivial when a = 0 or b = 0. We therefore make the following constructors available: PosSMulMono.of_pos, PosSMulReflectLT.of_pos, SMulPosMono.of_pos, SMulPosReflectLT.of_pos

Implications #

As α and β get 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!

Implementation notes #

This file uses custom typeclasses instead of abbreviations of CovariantClass/ContravariantClass because:

In the future, it would be good to make the corresponding typeclasses in Mathlib.Algebra.Order.Ring.Lemmas custom typeclasses too.

TODO #

This file acts as a substitute for Mathlib.Algebra.Order.SMul. We now need to

class PosSMulMono (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero α] :

Typeclass for monotonicity of scalar 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 OrderedSMul.

Instances
    class PosSMulStrictMono (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero α] :

    Typeclass for strict monotonicity of scalar 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 OrderedSMul.

    Instances
      class PosSMulReflectLT (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero α] :

      Typeclass for strict reverse monotonicity of scalar 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 OrderedSMul.

      Instances
        class PosSMulReflectLE (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero α] :

        Typeclass for reverse monotonicity of scalar 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 OrderedSMul.

        • elim : ∀ ⦃a : α⦄, 0 < a∀ ⦃b₁ b₂ : β⦄, a b₁ a b₂b₁ b₂

          Do not use this. Use le_of_smul_lt_smul_left instead.

        Instances
          class SMulPosMono (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero β] :

          Typeclass for monotonicity of scalar multiplication by nonnegative elements on the left, 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 OrderedSMul.

          Instances
            class SMulPosStrictMono (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero β] :

            Typeclass for strict monotonicity of scalar multiplication by positive elements on the left, 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 OrderedSMul.

            Instances
              class SMulPosReflectLT (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero β] :

              Typeclass for strict reverse monotonicity of scalar multiplication by nonnegative elements on the left, 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 OrderedSMul.

              Instances
                class SMulPosReflectLE (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero β] :

                Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left, 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 OrderedSMul.

                • elim : ∀ ⦃b : β⦄, 0 < b∀ ⦃a₁ a₂ : α⦄, a₁ b a₂ ba₁ a₂

                  Do not use this. Use le_of_smul_lt_smul_right instead.

                Instances
                  instance PosMulMono.toPosSMulMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulMono α] :
                  Equations
                  Equations
                  Equations
                  Equations
                  instance MulPosMono.toSMulPosMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosMono α] :
                  Equations
                  Equations
                  Equations
                  Equations
                  theorem monotone_smul_left_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] (ha : 0 a) :
                  Monotone fun (x : β) => a x
                  theorem strictMono_smul_left_of_pos {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] (ha : 0 < a) :
                  StrictMono fun (x : β) => a x
                  theorem smul_le_smul_of_nonneg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] (hb : b₁ b₂) (ha : 0 a) :
                  a b₁ a b₂
                  theorem smul_lt_smul_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : 0 < a) :
                  a b₁ < a b₂
                  theorem lt_of_smul_lt_smul_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLT α β] (h : a b₁ < a b₂) (ha : 0 a) :
                  b₁ < b₂
                  theorem le_of_smul_le_smul_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLE α β] (h : a b₁ a b₂) (ha : 0 < a) :
                  b₁ b₂
                  theorem lt_of_smul_lt_smul_of_nonneg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLT α β] (h : a b₁ < a b₂) (ha : 0 a) :
                  b₁ < b₂

                  Alias of lt_of_smul_lt_smul_left.

                  theorem le_of_smul_le_smul_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLE α β] (h : a b₁ a b₂) (ha : 0 < a) :
                  b₁ b₂

                  Alias of le_of_smul_le_smul_left.

                  @[simp]
                  theorem smul_le_smul_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                  a b₁ a b₂ b₁ b₂
                  @[simp]
                  theorem smul_lt_smul_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                  a b₁ < a b₂ b₁ < b₂
                  theorem monotone_smul_right_of_nonneg {α : Type u_1} {β : Type u_2} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosMono α β] (hb : 0 b) :
                  Monotone fun (x : α) => x b
                  theorem strictMono_smul_right_of_pos {α : Type u_1} {β : Type u_2} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] (hb : 0 < b) :
                  StrictMono fun (x : α) => x b
                  theorem smul_le_smul_of_nonneg_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosMono α β] (ha : a₁ a₂) (hb : 0 b) :
                  a₁ b a₂ b
                  theorem smul_lt_smul_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : 0 < b) :
                  a₁ b < a₂ b
                  theorem lt_of_smul_lt_smul_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLT α β] (h : a₁ b < a₂ b) (hb : 0 b) :
                  a₁ < a₂
                  theorem le_of_smul_le_smul_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLE α β] (h : a₁ b a₂ b) (hb : 0 < b) :
                  a₁ a₂
                  theorem lt_of_smul_lt_smul_of_nonneg_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLT α β] (h : a₁ b < a₂ b) (hb : 0 b) :
                  a₁ < a₂

                  Alias of lt_of_smul_lt_smul_right.

                  theorem le_of_smul_le_smul_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLE α β] (h : a₁ b a₂ b) (hb : 0 < b) :
                  a₁ a₂

                  Alias of le_of_smul_le_smul_right.

                  @[simp]
                  theorem smul_le_smul_iff_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
                  a₁ b a₂ b a₁ a₂
                  @[simp]
                  theorem smul_lt_smul_iff_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
                  a₁ b < a₂ b a₁ < a₂
                  theorem smul_lt_smul_of_le_of_lt {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosMono α β] (ha : a₁ a₂) (hb : b₁ < b₂) (h₁ : 0 < a₁) (h₂ : 0 b₂) :
                  a₁ b₁ < a₂ b₂
                  theorem smul_lt_smul_of_le_of_lt' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosMono α β] (ha : a₁ a₂) (hb : b₁ < b₂) (h₂ : 0 < a₂) (h₁ : 0 b₁) :
                  a₁ b₁ < a₂ b₂
                  theorem smul_lt_smul_of_lt_of_le {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : b₁ b₂) (h₁ : 0 a₁) (h₂ : 0 < b₂) :
                  a₁ b₁ < a₂ b₂
                  theorem smul_lt_smul_of_lt_of_le' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : b₁ b₂) (h₂ : 0 a₂) (h₁ : 0 < b₁) :
                  a₁ b₁ < a₂ b₂
                  theorem smul_lt_smul {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : b₁ < b₂) (h₁ : 0 < a₁) (h₂ : 0 < b₂) :
                  a₁ b₁ < a₂ b₂
                  theorem smul_lt_smul' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : b₁ < b₂) (h₂ : 0 < a₂) (h₁ : 0 < b₁) :
                  a₁ b₁ < a₂ b₂
                  theorem smul_le_smul {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosMono α β] (ha : a₁ a₂) (hb : b₁ b₂) (h₁ : 0 a₁) (h₂ : 0 b₂) :
                  a₁ b₁ a₂ b₂
                  theorem smul_le_smul' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosMono α β] (ha : a₁ a₂) (hb : b₁ b₂) (h₂ : 0 a₂) (h₁ : 0 b₁) :
                  a₁ b₁ a₂ b₂
                  instance PosSMulStrictMono.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulStrictMono α β] :
                  Equations
                  theorem PosSMulReflectLE.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulReflectLE α β] :
                  instance PosSMulMono.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] :
                  Equations
                  theorem PosSMulReflectLT.toPosSMulMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulReflectLT α β] :
                  theorem posSMulMono_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] :
                  theorem smul_max_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 a) (b₁ : β) (b₂ : β) :
                  a max b₁ b₂ = max (a b₁) (a b₂)
                  theorem smul_min_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 a) (b₁ : β) (b₂ : β) :
                  a min b₁ b₂ = min (a b₁) (a b₂)
                  theorem SMulPosReflectLE.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero β] [SMulPosReflectLE α β] :
                  theorem SMulPosReflectLT.toSMulPosMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero β] [SMulPosReflectLT α β] :
                  instance SMulPosStrictMono.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] :
                  Equations
                  theorem SMulPosMono.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [Preorder β] [Zero β] [SMulPosMono α β] :
                  theorem smulPosMono_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [LinearOrder β] [Zero β] :
                  theorem smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] (ha : 0 < a) (hb : 0 < b) :
                  0 < a b
                  theorem smul_neg_of_pos_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] (ha : 0 < a) (hb : b < 0) :
                  a b < 0
                  @[simp]
                  theorem smul_pos_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                  0 < a b 0 < b
                  theorem smul_neg_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                  a b < 0 b < 0
                  theorem smul_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] (ha : 0 a) (hb : 0 b₁) :
                  0 a b₁
                  theorem smul_nonpos_of_nonneg_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] (ha : 0 a) (hb : b 0) :
                  a b 0
                  theorem pos_of_smul_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulReflectLT α β] (h : 0 < a b) (ha : 0 a) :
                  0 < b
                  theorem neg_of_smul_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulReflectLT α β] (h : a b < 0) (ha : 0 a) :
                  b < 0
                  theorem smul_pos' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (ha : 0 < a) (hb : 0 < b) :
                  0 < a b
                  theorem smul_neg_of_neg_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (ha : a < 0) (hb : 0 < b) :
                  a b < 0
                  @[simp]
                  theorem smul_pos_iff_of_pos_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
                  0 < a b 0 < a
                  theorem smul_nonneg' {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosMono α β] (ha : 0 a) (hb : 0 b₁) :
                  0 a b₁
                  theorem smul_nonpos_of_nonpos_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosMono α β] (ha : a 0) (hb : 0 b) :
                  a b 0
                  theorem pos_of_smul_pos_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosReflectLT α β] (h : 0 < a b) (hb : 0 b) :
                  0 < a
                  theorem neg_of_smul_neg_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosReflectLT α β] (h : a b < 0) (hb : 0 b) :
                  a < 0
                  theorem pos_iff_pos_of_smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [PosSMulReflectLT α β] [SMulPosReflectLT α β] (hab : 0 < a b) :
                  0 < a 0 < b
                  theorem PosSMulMono.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [Preorder β] (h₀ : ∀ (a : α), 0 < a∀ (b₁ b₂ : β), b₁ b₂a b₁ a b₂) :

                  A constructor for PosSMulMono requiring you to prove b₁ ≤ b₂ → a • b₁ ≤ a • b₂ only when 0 < a

                  theorem PosSMulReflectLT.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [Preorder β] (h₀ : ∀ (a : α), 0 < a∀ (b₁ b₂ : β), a b₁ < a b₂b₁ < b₂) :

                  A constructor for PosSMulReflectLT requiring you to prove a • b₁ < a • b₂ → b₁ < b₂ only when 0 < a

                  theorem SMulPosMono.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [PartialOrder β] (h₀ : ∀ (b : β), 0 < b∀ (a₁ a₂ : α), a₁ a₂a₁ b a₂ b) :

                  A constructor for SMulPosMono requiring you to prove a₁ ≤ a₂ → a₁ • b ≤ a₂ • b only when 0 < b

                  theorem SMulPosReflectLT.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [PartialOrder β] (h₀ : ∀ (b : β), 0 < b∀ (a₁ a₂ : α), a₁ b < a₂ ba₁ < a₂) :

                  A constructor for SMulPosReflectLT requiring you to prove a₁ • b < a₂ • b → a₁ < a₂ only when 0 < b

                  instance PosSMulStrictMono.toPosSMulMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] :
                  Equations
                  instance SMulPosStrictMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosStrictMono α β] :
                  Equations
                  instance PosSMulReflectLE.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulReflectLE α β] :
                  Equations
                  instance SMulPosReflectLE.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosReflectLE α β] :
                  Equations
                  theorem smul_eq_smul_iff_eq_and_eq_of_pos {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (ha : a₁ a₂) (hb : b₁ b₂) (h₁ : 0 < a₁) (h₂ : 0 < b₂) :
                  a₁ b₁ = a₂ b₂ a₁ = a₂ b₁ = b₂
                  theorem smul_eq_smul_iff_eq_and_eq_of_pos' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (ha : a₁ a₂) (hb : b₁ b₂) (h₂ : 0 < a₂) (h₁ : 0 < b₁) :
                  a₁ b₁ = a₂ b₂ a₁ = a₂ b₁ = b₂
                  theorem pos_and_pos_or_neg_and_neg_of_smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (hab : 0 < a b) :
                  0 < a 0 < b a < 0 b < 0
                  theorem neg_of_smul_pos_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (h : 0 < a b) (ha : a 0) :
                  b < 0
                  theorem neg_of_smul_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (h : 0 < a b) (ha : b 0) :
                  a < 0
                  theorem neg_iff_neg_of_smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (hab : 0 < a b) :
                  a < 0 b < 0
                  theorem neg_of_smul_neg_left' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [SMulPosMono α β] (h : a b < 0) (ha : 0 a) :
                  b < 0
                  theorem neg_of_smul_neg_right' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] (h : a b < 0) (hb : 0 b) :
                  a < 0
                  @[simp]
                  theorem le_smul_iff_one_le_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
                  b a b 1 a
                  @[simp]
                  theorem lt_smul_iff_one_lt_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
                  b < a b 1 < a
                  @[simp]
                  theorem smul_le_iff_le_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
                  a b b a 1
                  @[simp]
                  theorem smul_lt_iff_lt_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
                  a b < b a < 1
                  theorem smul_le_of_le_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] (hb : 0 b) (h : a 1) :
                  a b b
                  theorem le_smul_of_one_le_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] (hb : 0 b) (h : 1 a) :
                  b a b
                  theorem smul_lt_of_lt_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (hb : 0 < b) (h : a < 1) :
                  a b < b
                  theorem lt_smul_of_one_lt_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (hb : 0 < b) (h : 1 < a) :
                  b < a b
                  Equations
                  theorem inv_smul_le_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                  a⁻¹ b₁ b₂ b₁ a b₂
                  theorem le_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                  b₁ a⁻¹ b₂ a b₁ b₂
                  theorem inv_smul_lt_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                  a⁻¹ b₁ < b₂ b₁ < a b₂
                  theorem lt_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                  b₁ < a⁻¹ b₂ a b₁ < b₂
                  @[simp]
                  theorem OrderIso.smulRight_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) :
                  @[simp]
                  theorem OrderIso.smulRight_symm_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) :
                  def OrderIso.smulRight {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) :
                  β ≃o β

                  Right scalar multiplication as an order isomorphism.

                  Equations
                  Instances For
                    instance OrderDual.instPosSMulMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulMono α β] :
                    Equations
                    instance OrderDual.instPosSMulStrictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulStrictMono α β] :
                    Equations
                    instance OrderDual.instPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulReflectLT α β] :
                    Equations
                    instance OrderDual.instPosSMulReflectLE {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulReflectLE α β] :
                    Equations
                    instance OrderDual.instSMulPosMono {α : Type u_1} {β : Type u_2} [Preorder α] [Ring α] [OrderedAddCommGroup β] [Module α β] [SMulPosMono α β] :
                    Equations
                    instance OrderDual.instSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Preorder α] [Ring α] [OrderedAddCommGroup β] [Module α β] [SMulPosReflectLT α β] :
                    Equations
                    instance OrderDual.instSMulPosReflectLE {α : Type u_1} {β : Type u_2} [Preorder α] [Ring α] [OrderedAddCommGroup β] [Module α β] [SMulPosReflectLE α β] :
                    Equations
                    theorem smul_le_smul_of_nonpos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] (h : b₁ b₂) (ha : a 0) :
                    a b₂ a b₁
                    theorem antitone_smul_left {α : Type u_1} {β : Type u_2} {a : α} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] (ha : a 0) :
                    Antitone fun (x : β) => a x
                    instance PosSMulMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] :
                    Equations
                    theorem smul_lt_smul_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : a < 0) :
                    a b₂ < a b₁
                    theorem strictAnti_smul_left {α : Type u_1} {β : Type u_2} {a : α} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] (ha : a < 0) :
                    StrictAnti fun (x : β) => a x
                    Equations
                    theorem le_of_smul_le_smul_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulReflectLE α β] (h : a b₁ a b₂) (ha : a < 0) :
                    b₂ b₁
                    theorem lt_of_smul_lt_smul_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulReflectLT α β] (h : a b₁ < a b₂) (ha : a 0) :
                    b₂ < b₁
                    theorem smul_nonneg_of_nonpos_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [SMulPosMono α β] (ha : a 0) (hb : b 0) :
                    0 a b
                    theorem smul_le_smul_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : a < 0) :
                    a b₁ a b₂ b₂ b₁
                    theorem smul_lt_smul_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                    a b₁ < a b₂ b₂ < b₁
                    theorem smul_pos_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                    0 < a b b < 0
                    theorem smul_pos_of_neg_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                    b < 00 < a b

                    Alias of the reverse direction of smul_pos_iff_of_neg_left.

                    theorem smul_neg_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                    a b < 0 0 < b
                    theorem smul_add_smul_le_smul_add_smul {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hab : b₁ b₂) (hcd : a d) :
                    b₁ d + b₂ a b₁ a + b₂ d

                    Binary rearrangement inequality.

                    theorem smul_add_smul_le_smul_add_smul' {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hba : b₂ b₁) (hdc : d a) :
                    b₁ d + b₂ a b₁ a + b₂ d

                    Binary rearrangement inequality.

                    theorem smul_add_smul_lt_smul_add_smul {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hab : b₁ < b₂) (hcd : a < d) :
                    b₁ d + b₂ a < b₁ a + b₂ d

                    Binary strict rearrangement inequality.

                    theorem smul_add_smul_lt_smul_add_smul' {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hba : b₂ < b₁) (hdc : d < a) :
                    b₁ d + b₂ a < b₁ a + b₂ d

                    Binary strict rearrangement inequality.

                    theorem smul_max_of_nonpos {α : Type u_1} {β : Type u_2} [OrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {a : α} (ha : a 0) (b₁ : β) (b₂ : β) :
                    a max b₁ b₂ = min (a b₁) (a b₂)
                    theorem smul_min_of_nonpos {α : Type u_1} {β : Type u_2} [OrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {a : α} (ha : a 0) (b₁ : β) (b₂ : β) :
                    a min b₁ b₂ = max (a b₁) (a b₂)
                    theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} (hab : 0 a b) :
                    0 a 0 b a 0 b 0
                    theorem smul_nonneg_iff {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
                    0 a b 0 a 0 b a 0 b 0
                    theorem smul_nonpos_iff {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
                    a b 0 0 a b 0 a 0 0 b
                    theorem smul_nonneg_iff_pos_imp_nonneg {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
                    0 a b (0 < a0 b) (0 < b0 a)
                    theorem smul_nonneg_iff_neg_imp_nonpos {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
                    0 a b (a < 0b 0) (b < 0a 0)
                    theorem smul_nonpos_iff_pos_imp_nonpos {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
                    a b 0 (0 < ab 0) (b < 00 a)
                    theorem smul_nonpos_iff_neg_imp_nonneg {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
                    a b 0 (a < 00 b) (0 < ba 0)
                    Equations
                    theorem inv_smul_le_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulMono α β] (h : a < 0) :
                    a⁻¹ b₁ b₂ a b₂ b₁
                    theorem smul_inv_le_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulMono α β] (h : a < 0) :
                    b₁ a⁻¹ b₂ b₂ a b₁
                    @[simp]
                    theorem OrderIso.smulRightDual_symm_apply {α : Type u_1} (β : Type u_2) [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} [PosSMulMono α β] (ha : a < 0) :
                    ∀ (a_1 : βᵒᵈ), (RelIso.symm (OrderIso.smulRightDual β ha)) a_1 = a⁻¹ OrderDual.ofDual a_1
                    @[simp]
                    theorem OrderIso.smulRightDual_apply {α : Type u_1} (β : Type u_2) [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} [PosSMulMono α β] (ha : a < 0) :
                    ∀ (a_1 : β), (OrderIso.smulRightDual β ha) a_1 = a OrderDual.toDual a_1
                    def OrderIso.smulRightDual {α : Type u_1} (β : Type u_2) [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} [PosSMulMono α β] (ha : a < 0) :

                    Left scalar multiplication as an order isomorphism.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem inv_smul_lt_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulStrictMono α β] (h : a < 0) :
                      a⁻¹ b₁ < b₂ a b₂ < b₁
                      theorem smul_inv_lt_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulStrictMono α β] (h : a < 0) :
                      b₁ < a⁻¹ b₂ b₂ < a b₁
                      instance Pi.instPosSMulMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), PosSMulMono α (β i)] :
                      PosSMulMono α ((i : ι) → β i)
                      Equations
                      instance Pi.instSMulPosMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [(i : ι) → Zero (β i)] [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), SMulPosMono α (β i)] :
                      SMulPosMono α ((i : ι) → β i)
                      Equations
                      instance Pi.instPosSMulReflectLE {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), PosSMulReflectLE α (β i)] :
                      PosSMulReflectLE α ((i : ι) → β i)
                      Equations
                      instance Pi.instSMulPosReflectLE {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [(i : ι) → Zero (β i)] [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), SMulPosReflectLE α (β i)] :
                      SMulPosReflectLE α ((i : ι) → β i)
                      Equations
                      instance Pi.instPosSMulStrictMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [PartialOrder α] [(i : ι) → PartialOrder (β i)] [(i : ι) → SMulWithZero α (β i)] [∀ (i : ι), PosSMulStrictMono α (β i)] :
                      PosSMulStrictMono α ((i : ι) → β i)
                      Equations
                      instance Pi.instSMulPosStrictMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [PartialOrder α] [(i : ι) → PartialOrder (β i)] [(i : ι) → SMulWithZero α (β i)] [∀ (i : ι), SMulPosStrictMono α (β i)] :
                      SMulPosStrictMono α ((i : ι) → β i)
                      Equations
                      instance Pi.instSMulPosReflectLT {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [PartialOrder α] [(i : ι) → PartialOrder (β i)] [(i : ι) → SMulWithZero α (β i)] [∀ (i : ι), SMulPosReflectLT α (β i)] :
                      SMulPosReflectLT α ((i : ι) → β i)
                      Equations
                      theorem PosSMulMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [PosSMulMono α γ] :
                      theorem PosSMulStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [PosSMulStrictMono α γ] :
                      theorem PosSMulReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [PosSMulReflectLE α γ] :
                      theorem PosSMulReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [PosSMulReflectLT α γ] :
                      theorem SMulPosMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Zero β] [Preorder β] [Zero γ] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [SMulPosMono α γ] :
                      theorem SMulPosStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Zero β] [Preorder β] [Zero γ] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [SMulPosStrictMono α γ] :
                      theorem SMulPosReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Zero β] [Preorder β] [Zero γ] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [SMulPosReflectLE α γ] :
                      theorem SMulPosReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Zero β] [Preorder β] [Zero γ] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [SMulPosReflectLT α γ] :

                      Positivity extension for HSMul, i.e. (_ • _).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Deprecated lemmas #

                        Those lemmas have been deprecated on 2023-12-23.

                        @[deprecated monotone_smul_left_of_nonneg]
                        theorem monotone_smul_left {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] (ha : 0 a) :
                        Monotone fun (x : β) => a x

                        Alias of monotone_smul_left_of_nonneg.

                        @[deprecated strictMono_smul_left_of_pos]
                        theorem strict_mono_smul_left {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] (ha : 0 < a) :
                        StrictMono fun (x : β) => a x

                        Alias of strictMono_smul_left_of_pos.

                        @[deprecated smul_le_smul_of_nonneg_left]
                        theorem smul_le_smul_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] (hb : b₁ b₂) (ha : 0 a) :
                        a b₁ a b₂

                        Alias of smul_le_smul_of_nonneg_left.

                        @[deprecated smul_lt_smul_of_pos_left]
                        theorem smul_lt_smul_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : 0 < a) :
                        a b₁ < a b₂

                        Alias of smul_lt_smul_of_pos_left.

                        @[deprecated lt_of_smul_lt_smul_of_nonneg_left]
                        theorem lt_of_smul_lt_smul_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLT α β] (h : a b₁ < a b₂) (ha : 0 a) :
                        b₁ < b₂

                        Alias of lt_of_smul_lt_smul_left.


                        Alias of lt_of_smul_lt_smul_left.

                        @[deprecated smul_le_smul_iff_of_pos_left]
                        theorem smul_le_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                        a b₁ a b₂ b₁ b₂

                        Alias of smul_le_smul_iff_of_pos_left.

                        @[deprecated smul_lt_smul_iff_of_pos_left]
                        theorem smul_lt_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                        a b₁ < a b₂ b₁ < b₂

                        Alias of smul_lt_smul_iff_of_pos_left.

                        @[deprecated smul_max_of_nonneg]
                        theorem smul_max {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 a) (b₁ : β) (b₂ : β) :
                        a max b₁ b₂ = max (a b₁) (a b₂)

                        Alias of smul_max_of_nonneg.

                        @[deprecated smul_min_of_nonneg]
                        theorem smul_min {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 a) (b₁ : β) (b₂ : β) :
                        a min b₁ b₂ = min (a b₁) (a b₂)

                        Alias of smul_min_of_nonneg.

                        @[deprecated smul_pos_iff_of_pos_left]
                        theorem smul_pos_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                        0 < a b 0 < b

                        Alias of smul_pos_iff_of_pos_left.

                        @[deprecated inv_smul_le_iff_of_pos]
                        theorem inv_smul_le_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                        a⁻¹ b₁ b₂ b₁ a b₂

                        Alias of inv_smul_le_iff_of_pos.

                        @[deprecated le_inv_smul_iff_of_pos]
                        theorem le_inv_smul_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                        b₁ a⁻¹ b₂ a b₁ b₂

                        Alias of le_inv_smul_iff_of_pos.

                        @[deprecated inv_smul_lt_iff_of_pos]
                        theorem inv_smul_lt_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                        a⁻¹ b₁ < b₂ b₁ < a b₂

                        Alias of inv_smul_lt_iff_of_pos.

                        @[deprecated lt_inv_smul_iff_of_pos]
                        theorem lt_inv_smul_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                        b₁ < a⁻¹ b₂ a b₁ < b₂

                        Alias of lt_inv_smul_iff_of_pos.

                        @[deprecated OrderIso.smulRight]
                        def OrderIso.smulLeft {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) :
                        β ≃o β

                        Alias of OrderIso.smulRight.


                        Right scalar multiplication as an order isomorphism.

                        Equations
                        Instances For
                          @[deprecated OrderIso.smulRight_symm_apply]
                          theorem OrderIso.smulLeft_symm_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) :

                          Alias of OrderIso.smulRight_symm_apply.

                          @[deprecated OrderIso.smulRight_apply]
                          theorem OrderIso.smulLeft_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) :

                          Alias of OrderIso.smulRight_apply.

                          @[deprecated smul_neg_iff_of_pos_left]
                          theorem smul_neg_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
                          a b < 0 b < 0

                          Alias of smul_neg_iff_of_pos_left.

                          Those lemmas have been deprecated on 2023-12-27.

                          @[deprecated strictAnti_smul_left]
                          theorem strict_anti_smul_left {α : Type u_1} {β : Type u_2} {a : α} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] (ha : a < 0) :
                          StrictAnti fun (x : β) => a x

                          Alias of strictAnti_smul_left.

                          @[deprecated smul_le_smul_of_nonpos_left]
                          theorem smul_le_smul_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] (h : b₁ b₂) (ha : a 0) :
                          a b₂ a b₁

                          Alias of smul_le_smul_of_nonpos_left.

                          @[deprecated smul_lt_smul_of_neg_left]
                          theorem smul_lt_smul_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : a < 0) :
                          a b₂ < a b₁

                          Alias of smul_lt_smul_of_neg_left.

                          @[deprecated smul_pos_iff_of_neg_left]
                          theorem smul_pos_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                          0 < a b b < 0

                          Alias of smul_pos_iff_of_neg_left.

                          @[deprecated smul_neg_iff_of_neg_left]
                          theorem smul_neg_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                          a b < 0 0 < b

                          Alias of smul_neg_iff_of_neg_left.

                          @[deprecated smul_le_smul_iff_of_neg_left]
                          theorem smul_le_smul_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : a < 0) :
                          a b₁ a b₂ b₂ b₁

                          Alias of smul_le_smul_iff_of_neg_left.

                          @[deprecated smul_lt_smul_iff_of_neg_left]
                          theorem smul_lt_smul_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
                          a b₁ < a b₂ b₂ < b₁

                          Alias of smul_lt_smul_iff_of_neg_left.