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:

Unless otherwise stated, all these implications 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.GroupWithZero.Unbundled 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
    theorem PosSMulMono.elim {α : Type u_1} {β : Type u_2} :
    ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulMono α β] ⦃a : α⦄, 0 a∀ ⦃b₁ b₂ : β⦄, b₁ b₂a b₁ a b₂

    Do not use this. Use smul_le_smul_of_nonneg_left instead.

    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
      theorem PosSMulStrictMono.elim {α : Type u_1} {β : Type u_2} :
      ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulStrictMono α β] ⦃a : α⦄, 0 < a∀ ⦃b₁ b₂ : β⦄, b₁ < b₂a b₁ < a b₂

      Do not use this. Use smul_lt_smul_of_pos_left instead.

      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
        theorem PosSMulReflectLT.elim {α : Type u_1} {β : Type u_2} :
        ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulReflectLT α β] ⦃a : α⦄, 0 a∀ ⦃b₁ b₂ : β⦄, a b₁ < a b₂b₁ < b₂

        Do not use this. Use lt_of_smul_lt_smul_left instead.

        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
          theorem PosSMulReflectLE.elim {α : Type u_1} {β : Type u_2} :
          ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulReflectLE α β] ⦃a : α⦄, 0 < a∀ ⦃b₁ b₂ : β⦄, a b₁ a b₂b₁ b₂

          Do not use this. Use le_of_smul_lt_smul_left instead.

          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
            theorem SMulPosMono.elim {α : Type u_1} {β : Type u_2} :
            ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosMono α β] ⦃b : β⦄, 0 b∀ ⦃a₁ a₂ : α⦄, a₁ a₂a₁ b a₂ b

            Do not use this. Use smul_le_smul_of_nonneg_right instead.

            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
              theorem SMulPosStrictMono.elim {α : Type u_1} {β : Type u_2} :
              ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosStrictMono α β] ⦃b : β⦄, 0 < b∀ ⦃a₁ a₂ : α⦄, a₁ < a₂a₁ b < a₂ b

              Do not use this. Use smul_lt_smul_of_pos_right instead.

              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
                theorem SMulPosReflectLT.elim {α : Type u_1} {β : Type u_2} :
                ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosReflectLT α β] ⦃b : β⦄, 0 b∀ ⦃a₁ a₂ : α⦄, a₁ b < a₂ ba₁ < a₂

                Do not use this. Use lt_of_smul_lt_smul_right instead.

                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
                  theorem SMulPosReflectLE.elim {α : Type u_1} {β : Type u_2} :
                  ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosReflectLE α β] ⦃b : β⦄, 0 < b∀ ⦃a₁ a₂ : α⦄, a₁ b a₂ ba₁ a₂

                  Do not use this. Use le_of_smul_lt_smul_right instead.

                  @[instance 100]
                  instance PosMulMono.toPosSMulMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulMono α] :
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  instance MulPosMono.toSMulPosMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosMono α] :
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  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 100]
                  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 100]
                  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 100]
                  instance PosSMulStrictMono.toPosSMulMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] :
                  Equations
                  • =
                  @[instance 100]
                  instance SMulPosStrictMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosStrictMono α β] :
                  Equations
                  • =
                  @[instance 100]
                  instance PosSMulReflectLE.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulReflectLE α β] :
                  Equations
                  • =
                  @[instance 100]
                  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_symm_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) :
                  @[simp]
                  theorem OrderIso.smulRight_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 α] [Monoid α] [OrderedAddCommGroup β] [DistribMulAction α β] [SMulPosMono α β] :
                    Equations
                    • =
                    Equations
                    • =
                    Equations
                    • =
                    Equations
                    • =
                    theorem smul_add_smul_le_smul_add_smul {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₁ a₂) (hb : b₁ b₂) :
                    a₁ b₂ + a₂ b₁ a₁ b₁ + a₂ b₂

                    Binary rearrangement inequality.

                    theorem smul_add_smul_le_smul_add_smul' {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₂ a₁) (hb : b₂ b₁) :
                    a₁ b₂ + a₂ b₁ a₁ b₁ + a₂ b₂

                    Binary rearrangement inequality.

                    theorem smul_add_smul_lt_smul_add_smul {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulStrictMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₁ < a₂) (hb : b₁ < b₂) :
                    a₁ b₂ + a₂ b₁ < a₁ b₁ + a₂ b₂

                    Binary strict rearrangement inequality.

                    theorem smul_add_smul_lt_smul_add_smul' {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulStrictMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₂ < a₁) (hb : b₂ < b₁) :
                    a₁ b₂ + a₂ b₁ < a₁ b₁ + a₂ b₂

                    Binary strict rearrangement inequality.

                    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_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)
                    @[instance 100]
                    Equations
                    • =
                    @[instance 100]
                    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_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
                    @[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
                    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
                    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} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero α] [PosSMulMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) :
                      theorem PosSMulStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero α] [PosSMulStrictMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) :
                      theorem PosSMulReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero α] [PosSMulReflectLE α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) :
                      theorem PosSMulReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero α] [PosSMulReflectLT α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) :
                      theorem SMulPosMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero β] [Zero γ] [SMulPosMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) :
                      theorem SMulPosStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero β] [Zero γ] [SMulPosStrictMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) :
                      theorem SMulPosReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero β] [Zero γ] [SMulPosReflectLE α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) :
                      theorem SMulPosReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : βγ) [Zero β] [Zero γ] [SMulPosReflectLT α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) :
                      Equations
                      • =
                      Equations
                      • =

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

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