Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Nat.instMulLeftMono instance

: MulLeftMono ℕ

Full source

instance Nat.instMulLeftMono : MulLeftMono ℕ where
  elim := fun _ _ _ h => mul_le_mul_left _ h

Left-Multiplicative Monotonicity of Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a left-multiplicative monotone structure, meaning that for any $a, b, c \in \mathbb{N}$, if $b \leq c$, then $a \cdot b \leq a \cdot c$.

Int.instAddLeftMono instance

: AddLeftMono ℤ

Full source

instance Int.instAddLeftMono : AddLeftMono ℤ where
  elim := fun _ _ _ h => Int.add_le_add_left h _

Additive Left-Monotonicity of Integers

Informal description

The integers $\mathbb{Z}$ form an additive left-monotonic structure, meaning that for any integers $a, b, c$, if $b \leq c$, then $a + b \leq a + c$.

mul_le_mul_left' theorem

[MulLeftMono α] {b c : α} (bc : b ≤ c) (a : α) : a * b ≤ a * c

Full source

@[to_additive (attr := gcongr) add_le_add_left]
theorem mul_le_mul_left' [MulLeftMono α] {b c : α} (bc : b ≤ c) (a : α) :
    a * b ≤ a * c :=
  CovariantClass.elim _ bc

Left multiplication preserves order in left-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $b, c \in \alpha$ with $b \leq c$, and any element $a \in \alpha$, we have $a \cdot b \leq a \cdot c$.

le_of_mul_le_mul_left' theorem

[MulLeftReflectLE α] {a b c : α} (bc : a * b ≤ a * c) : b ≤ c

Full source

@[to_additive le_of_add_le_add_left]
theorem le_of_mul_le_mul_left' [MulLeftReflectLE α] {a b c : α}
    (bc : a * b ≤ a * c) :
    b ≤ c :=
  ContravariantClass.elim _ bc

Left Multiplication Reflects Order: $a \cdot b \leq a \cdot c \implies b \leq c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication on the left reflects the order (i.e., satisfies the condition `MulLeftReflectLE`). For any elements $a, b, c \in \alpha$, if $a \cdot b \leq a \cdot c$, then $b \leq c$.

mul_le_mul_right' theorem

[i : MulRightMono α] {b c : α} (bc : b ≤ c) (a : α) : b * a ≤ c * a

Full source

@[to_additive (attr := gcongr) add_le_add_right]
theorem mul_le_mul_right' [i : MulRightMono α] {b c : α} (bc : b ≤ c)
    (a : α) :
    b * a ≤ c * a :=
  i.elim a bc

Right multiplication preserves order in right-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $b, c \in \alpha$ with $b \leq c$, and any element $a \in \alpha$, we have $b \cdot a \leq c \cdot a$.

le_of_mul_le_mul_right' theorem

[i : MulRightReflectLE α] {a b c : α} (bc : b * a ≤ c * a) : b ≤ c

Full source

@[to_additive le_of_add_le_add_right]
theorem le_of_mul_le_mul_right' [i : MulRightReflectLE α] {a b c : α}
    (bc : b * a ≤ c * a) :
    b ≤ c :=
  i.elim a bc

Right Multiplication Reflects Order: $b \cdot a \leq c \cdot a \implies b \leq c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication on the right reflects the order (i.e., satisfies the condition `MulRightReflectLE`). For any elements $b, c, a \in \alpha$, if $b \cdot a \leq c \cdot a$, then $b \leq c$.

mul_le_mul_iff_left theorem

[MulLeftMono α] [MulLeftReflectLE α] (a : α) {b c : α} : a * b ≤ a * c ↔ b ≤ c

Full source

@[to_additive (attr := simp)]
theorem mul_le_mul_iff_left [MulLeftMono α]
    [MulLeftReflectLE α] (a : α) {b c : α} :
    a * b ≤ a * c ↔ b ≤ c :=
  rel_iff_cov α α (· * ·) (· ≤ ·) a

Left Multiplication Preserves/Reflects Order: $a * b \leq a * c \leftrightarrow b \leq c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order. Assume that multiplication on the left is monotone and reflects the order (i.e., for any $a$, the function $x \mapsto a * x$ is order-preserving and order-reflecting). Then for any element $a$ and any elements $b, c$ in $\alpha$, we have the equivalence: \[ a * b \leq a * c \leftrightarrow b \leq c. \]

mul_le_mul_iff_right theorem

[MulRightMono α] [MulRightReflectLE α] (a : α) {b c : α} : b * a ≤ c * a ↔ b ≤ c

Full source

@[to_additive (attr := simp)]
theorem mul_le_mul_iff_right [MulRightMono α]
    [MulRightReflectLE α] (a : α) {b c : α} :
    b * a ≤ c * a ↔ b ≤ c :=
  rel_iff_cov α α (swap (· * ·)) (· ≤ ·) a

Right Multiplication Preserves/Reflects Order: $b \cdot a \leq c \cdot a \leftrightarrow b \leq c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication is monotone and order-reflecting in the right argument. Then for any element $a \in \alpha$ and any elements $b, c \in \alpha$, we have the equivalence: \[ b \cdot a \leq c \cdot a \leftrightarrow b \leq c. \]

mul_lt_mul_iff_left theorem

[MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b c : α} : a * b < a * c ↔ b < c

Full source

@[to_additive (attr := simp)]
theorem mul_lt_mul_iff_left [MulLeftStrictMono α]
    [MulLeftReflectLT α] (a : α) {b c : α} :
    a * b < a * c ↔ b < c :=
  rel_iff_cov α α (· * ·) (· < ·) a

Strict Left Multiplication Preserves Order Iff

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict partial order, such that multiplication is strictly monotone in the left argument and reflects the strict order in the left argument. Then for any element $a \in \alpha$ and any elements $b, c \in \alpha$, we have $a \cdot b < a \cdot c$ if and only if $b < c$.

mul_lt_mul_iff_right theorem

[MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b c : α} : b * a < c * a ↔ b < c

Full source

@[to_additive (attr := simp)]
theorem mul_lt_mul_iff_right [MulRightStrictMono α]
    [MulRightReflectLT α] (a : α) {b c : α} :
    b * a < c * a ↔ b < c :=
  rel_iff_cov α α (swap (· * ·)) (· < ·) a

Strict Right Multiplication Preserves Order Iff

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication is strictly monotone in the right argument and reflects the strict order in the right argument. Then for any element $a \in \alpha$ and any elements $b, c \in \alpha$, we have $b \cdot a < c \cdot a$ if and only if $b < c$.

mul_lt_mul_left' theorem

[MulLeftStrictMono α] {b c : α} (bc : b < c) (a : α) : a * b < a * c

Full source

@[to_additive (attr := gcongr) add_lt_add_left]
theorem mul_lt_mul_left' [MulLeftStrictMono α] {b c : α} (bc : b < c) (a : α) :
    a * b < a * c :=
  CovariantClass.elim _ bc

Left multiplication preserves strict inequality under left strict monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If multiplication on the left is strictly monotone (i.e., the function $x \mapsto a * x$ is strictly increasing for any fixed $a$), then for any elements $b, c \in \alpha$ with $b < c$ and any element $a \in \alpha$, we have $a * b < a * c$.

lt_of_mul_lt_mul_left' theorem

[MulLeftReflectLT α] {a b c : α} (bc : a * b < a * c) : b < c

Full source

@[to_additive lt_of_add_lt_add_left]
theorem lt_of_mul_lt_mul_left' [MulLeftReflectLT α] {a b c : α}
    (bc : a * b < a * c) :
    b < c :=
  ContravariantClass.elim _ bc

Left Multiplication Reflects Strict Order: $a * b < a * c \to b < c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication on the left reflects the strict order (i.e., $a * b < a * c$ implies $b < c$). Then for any elements $a, b, c \in \alpha$, if $a * b < a * c$, it follows that $b < c$.

mul_lt_mul_right' theorem

[i : MulRightStrictMono α] {b c : α} (bc : b < c) (a : α) : b * a < c * a

Full source

@[to_additive (attr := gcongr) add_lt_add_right]
theorem mul_lt_mul_right' [i : MulRightStrictMono α] {b c : α} (bc : b < c)
    (a : α) :
    b * a < c * a :=
  i.elim a bc

Right multiplication preserves strict inequality under right strict monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If multiplication on the right is strictly monotone (i.e., the function $x \mapsto x * a$ is strictly increasing for any fixed $a$), then for any elements $b, c \in \alpha$ with $b < c$ and any element $a \in \alpha$, we have $b * a < c * a$.

lt_of_mul_lt_mul_right' theorem

[i : MulRightReflectLT α] {a b c : α} (bc : b * a < c * a) : b < c

Full source

@[to_additive lt_of_add_lt_add_right]
theorem lt_of_mul_lt_mul_right' [i : MulRightReflectLT α] {a b c : α}
    (bc : b * a < c * a) :
    b < c :=
  i.elim a bc

Right Multiplication Reflects Strict Order: $b * a < c * a \to b < c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication on the right reflects the strict order (i.e., $b * a < c * a$ implies $b < c$). Then for any elements $a, b, c \in \alpha$, if $b * a < c * a$, it follows that $b < c$.

mul_left_mono theorem

[MulLeftMono α] {a : α} : Monotone (a * ·)

Full source

@[to_additive]
lemma mul_left_mono [MulLeftMono α] {a : α} : Monotone (a * ·) :=
  fun _ _ h ↦ mul_le_mul_left' h _

Left Multiplication is Monotone: $b \leq c \to a \cdot b \leq a \cdot c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any fixed element $a \in \alpha$, the function $x \mapsto a \cdot x$ is monotone.

mul_right_mono theorem

[MulRightMono α] {a : α} : Monotone (· * a)

Full source

@[to_additive]
lemma mul_right_mono [MulRightMono α] {a : α} : Monotone (· * a) :=
  fun _ _ h ↦ mul_le_mul_right' h _

Right Multiplication is Monotone: $b \leq c \to b * a \leq c * a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication on the right is monotone (i.e., for any fixed $a \in \alpha$, the function $x \mapsto x * a$ is monotone). Then for any $a \in \alpha$, the function $x \mapsto x * a$ is monotone, meaning that for any $b, c \in \alpha$, $b \leq c$ implies $b * a \leq c * a$.

mul_left_strictMono theorem

[MulLeftStrictMono α] {a : α} : StrictMono (a * ·)

Full source

@[to_additive]
lemma mul_left_strictMono [MulLeftStrictMono α] {a : α} : StrictMono (a * ·) :=
  fun _ _ h ↦ mul_lt_mul_left' h _

Left Multiplication is Strictly Monotone: $b < c \implies a \cdot b < a \cdot c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If multiplication on the left is strictly monotone (i.e., the function $x \mapsto a * x$ is strictly increasing for any fixed $a$), then for any fixed element $a \in \alpha$, the function $x \mapsto a * x$ is strictly monotone. This means that for any $b, c \in \alpha$, $b < c$ implies $a * b < a * c$.

mul_right_strictMono theorem

[MulRightStrictMono α] {a : α} : StrictMono (· * a)

Full source

@[to_additive]
lemma mul_right_strictMono [MulRightStrictMono α] {a : α} : StrictMono (· * a) :=
  fun _ _ h ↦ mul_lt_mul_right' h _

Right Multiplication is Strictly Monotone: $b < c \implies b \cdot a < c \cdot a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If multiplication on the right is strictly monotone (i.e., the function $x \mapsto x * a$ is strictly increasing for any fixed $a$), then for any fixed element $a \in \alpha$, the function $x \mapsto x * a$ is strictly monotone. This means that for any $b, c \in \alpha$, $b < c$ implies $b * a < c * a$.

mul_lt_mul_of_lt_of_lt theorem

[MulLeftStrictMono α] [MulRightStrictMono α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d

Full source

@[to_additive (attr := gcongr)]
theorem mul_lt_mul_of_lt_of_lt [MulLeftStrictMono α]
    [MulRightStrictMono α]
    {a b c d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d :=
  calc
    a * c < a * d := mul_lt_mul_left' h₂ a
    _ < b * d := mul_lt_mul_right' h₁ d

Strict Inequality Preservation under Strictly-Monotone Multiplication: $a < b \land c < d \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order such that multiplication is both left-strictly-monotone (i.e., $x \mapsto a \cdot x$ is strictly increasing for any fixed $a$) and right-strictly-monotone (i.e., $x \mapsto x \cdot a$ is strictly increasing for any fixed $a$). Then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_le_of_lt theorem

[MulLeftStrictMono α] [MulRightMono α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) : a * c < b * d

Full source

@[to_additive]
theorem mul_lt_mul_of_le_of_lt [MulLeftStrictMono α]
    [MulRightMono α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :
    a * c < b * d :=
  (mul_le_mul_right' h₁ _).trans_lt (mul_lt_mul_left' h₂ b)

Strict Inequality Preservation under Left-Strictly-Monotone and Right-Monotone Multiplication: $a \leq b \land c < d \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a \leq b$ and $c < d$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_lt_of_le theorem

[MulLeftMono α] [MulRightStrictMono α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) : a * c < b * d

Full source

@[to_additive]
theorem mul_lt_mul_of_lt_of_le [MulLeftMono α]
    [MulRightStrictMono α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :
    a * c < b * d :=
  (mul_le_mul_left' h₂ _).trans_lt (mul_lt_mul_right' h₁ d)

Strict Inequality Preservation under Left-Monotone and Right-Strictly-Monotone Multiplication: $a < b \land c \leq d \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c \leq d$, we have $a \cdot c < b \cdot d$.

Left.mul_lt_mul theorem

[MulLeftStrictMono α] [MulRightMono α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d

Full source

/-- Only assumes left strict covariance. -/
@[to_additive "Only assumes left strict covariance"]
theorem Left.mul_lt_mul [MulLeftStrictMono α]
    [MulRightMono α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
    a * c < b * d :=
  mul_lt_mul_of_le_of_lt h₁.le h₂

Strict Inequality Preservation under Left-Strictly-Monotone and Right-Monotone Multiplication: $a < b \land c < d \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, we have $a \cdot c < b \cdot d$.

Right.mul_lt_mul theorem

[MulLeftMono α] [MulRightStrictMono α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d

Full source

/-- Only assumes right strict covariance. -/
@[to_additive "Only assumes right strict covariance"]
theorem Right.mul_lt_mul [MulLeftMono α]
    [MulRightStrictMono α] {a b c d : α}
    (h₁ : a < b) (h₂ : c < d) :
    a * c < b * d :=
  mul_lt_mul_of_lt_of_le h₁ h₂.le

Strict Inequality Preservation under Left-Monotone and Right-Strictly-Monotone Multiplication: $a < b \land c < d \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, we have $a \cdot c < b \cdot d$.

mul_le_mul' theorem

[MulLeftMono α] [MulRightMono α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d

Full source

@[to_additive (attr := gcongr) add_le_add]
theorem mul_le_mul' [MulLeftMono α] [MulRightMono α]
    {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
    a * c ≤ b * d :=
  (mul_le_mul_left' h₂ _).trans (mul_le_mul_right' h₁ d)

Multiplication Preserves Order in Bi-Monotone Structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a \leq b$ and $c \leq d$, we have $a \cdot c \leq b \cdot d$.

mul_le_mul_three theorem

 [MulLeftMono α] [MulRightMono α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a * b * c ≤ d * e * f

Full source

@[to_additive]
theorem mul_le_mul_three [MulLeftMono α]
    [MulRightMono α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e)
    (h₃ : c ≤ f) :
    a * b * c ≤ d * e * f :=
  mul_le_mul' (mul_le_mul' h₁ h₂) h₃

Triple Multiplication Preserves Order in Bi-Monotone Structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c, d, e, f \in \alpha$ with $a \leq d$, $b \leq e$, and $c \leq f$, we have $a \cdot b \cdot c \leq d \cdot e \cdot f$.

mul_lt_of_mul_lt_left theorem

[MulLeftMono α] {a b c d : α} (h : a * b < c) (hle : d ≤ b) : a * d < c

Full source

@[to_additive]
theorem mul_lt_of_mul_lt_left [MulLeftMono α] {a b c d : α} (h : a * b < c)
    (hle : d ≤ b) :
    a * d < c :=
  (mul_le_mul_left' hle a).trans_lt h

Left multiplication preserves strict inequality under left-monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ such that $a \cdot b < c$ and $d \leq b$, we have $a \cdot d < c$.

mul_le_of_mul_le_left theorem

[MulLeftMono α] {a b c d : α} (h : a * b ≤ c) (hle : d ≤ b) : a * d ≤ c

Full source

@[to_additive]
theorem mul_le_of_mul_le_left [MulLeftMono α] {a b c d : α} (h : a * b ≤ c)
    (hle : d ≤ b) :
    a * d ≤ c :=
  @act_rel_of_rel_of_act_rel _ _ _ (· ≤ ·) _ _ a _ _ _ hle h

Left multiplication preserves inequality under left-monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ such that $a \cdot b \leq c$ and $d \leq b$, we have $a \cdot d \leq c$.

mul_lt_of_mul_lt_right theorem

[MulRightMono α] {a b c d : α} (h : a * b < c) (hle : d ≤ a) : d * b < c

Full source

@[to_additive]
theorem mul_lt_of_mul_lt_right [MulRightMono α] {a b c d : α}
    (h : a * b < c) (hle : d ≤ a) :
    d * b < c :=
  (mul_le_mul_right' hle b).trans_lt h

Right-monotone multiplication preserves strict inequality: $a \cdot b < c$ and $d \leq a$ implies $d \cdot b < c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is right-monotone (i.e., $d \leq a$ implies $d \cdot b \leq a \cdot b$ for any $b$). For any elements $a, b, c, d \in \alpha$, if $a \cdot b < c$ and $d \leq a$, then $d \cdot b < c$.

mul_le_of_mul_le_right theorem

[MulRightMono α] {a b c d : α} (h : a * b ≤ c) (hle : d ≤ a) : d * b ≤ c

Full source

@[to_additive]
theorem mul_le_of_mul_le_right [MulRightMono α] {a b c d : α}
    (h : a * b ≤ c) (hle : d ≤ a) :
    d * b ≤ c :=
  (mul_le_mul_right' hle b).trans h

Right-monotone multiplication preserves inequality: $a \cdot b \leq c$ and $d \leq a$ implies $d \cdot b \leq c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is right-monotone (i.e., $d \leq a$ implies $d \cdot b \leq a \cdot b$ for any $b$). For any elements $a, b, c, d \in \alpha$, if $a \cdot b \leq c$ and $d \leq a$, then $d \cdot b \leq c$.

lt_mul_of_lt_mul_left theorem

[MulLeftMono α] {a b c d : α} (h : a < b * c) (hle : c ≤ d) : a < b * d

Full source

@[to_additive]
theorem lt_mul_of_lt_mul_left [MulLeftMono α] {a b c d : α} (h : a < b * c)
    (hle : c ≤ d) :
    a < b * d :=
  h.trans_le (mul_le_mul_left' hle b)

Left-monotone multiplication preserves strict inequality: $a < b \cdot c$ and $c \leq d$ implies $a < b \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is left-monotone (i.e., $c \leq d$ implies $b \cdot c \leq b \cdot d$ for any $b$). For any elements $a, b, c, d \in \alpha$, if $a < b \cdot c$ and $c \leq d$, then $a < b \cdot d$.

le_mul_of_le_mul_left theorem

[MulLeftMono α] {a b c d : α} (h : a ≤ b * c) (hle : c ≤ d) : a ≤ b * d

Full source

@[to_additive]
theorem le_mul_of_le_mul_left [MulLeftMono α] {a b c d : α} (h : a ≤ b * c)
    (hle : c ≤ d) :
    a ≤ b * d :=
  @rel_act_of_rel_of_rel_act _ _ _ (· ≤ ·) _ _ b _ _ _ hle h

Left-monotone multiplication preserves inequality: $a \leq b * c$ and $c \leq d$ implies $a \leq b * d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is left-monotone (i.e., $c \leq d$ implies $b * c \leq b * d$ for all $b$). For any elements $a, b, c, d \in \alpha$, if $a \leq b * c$ and $c \leq d$, then $a \leq b * d$.

lt_mul_of_lt_mul_right theorem

[MulRightMono α] {a b c d : α} (h : a < b * c) (hle : b ≤ d) : a < d * c

Full source

@[to_additive]
theorem lt_mul_of_lt_mul_right [MulRightMono α] {a b c d : α}
    (h : a < b * c) (hle : b ≤ d) :
    a < d * c :=
  h.trans_le (mul_le_mul_right' hle c)

Right-monotone multiplication preserves strict inequality: $a < b \cdot c$ and $b \leq d$ implies $a < d \cdot c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is right-monotone (i.e., $b \leq d$ implies $b \cdot c \leq d \cdot c$ for any $c$). For any elements $a, b, c, d \in \alpha$, if $a < b \cdot c$ and $b \leq d$, then $a < d \cdot c$.

le_mul_of_le_mul_right theorem

[MulRightMono α] {a b c d : α} (h : a ≤ b * c) (hle : b ≤ d) : a ≤ d * c

Full source

@[to_additive]
theorem le_mul_of_le_mul_right [MulRightMono α] {a b c d : α}
    (h : a ≤ b * c) (hle : b ≤ d) :
    a ≤ d * c :=
  h.trans (mul_le_mul_right' hle c)

Right-monotone multiplication preserves inequality: $a \leq b \cdot c$ and $b \leq d$ implies $a \leq d \cdot c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is right-monotone (i.e., $b \leq d$ implies $b \cdot c \leq d \cdot c$ for all $c$). For any elements $a, b, c, d \in \alpha$, if $a \leq b \cdot c$ and $b \leq d$, then $a \leq d \cdot c$.

mul_left_cancel'' theorem

[MulLeftReflectLE α] {a b c : α} (h : a * b = a * c) : b = c

Full source

@[to_additive]
theorem mul_left_cancel'' [MulLeftReflectLE α] {a b c : α} (h : a * b = a * c) :
    b = c :=
  (le_of_mul_le_mul_left' h.le).antisymm (le_of_mul_le_mul_left' h.ge)

Left Cancellation in Ordered Monoids: $a \cdot b = a \cdot c \implies b = c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication on the left reflects the order (i.e., satisfies the condition `MulLeftReflectLE`). For any elements $a, b, c \in \alpha$, if $a \cdot b = a \cdot c$, then $b = c$.

mul_right_cancel'' theorem

[MulRightReflectLE α] {a b c : α} (h : a * b = c * b) : a = c

Full source

@[to_additive]
theorem mul_right_cancel'' [MulRightReflectLE α] {a b c : α}
    (h : a * b = c * b) :
    a = c :=
  (le_of_mul_le_mul_right' h.le).antisymm (le_of_mul_le_mul_right' h.ge)

Right Cancellation in Ordered Monoids: $a \cdot b = c \cdot b \implies a = c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication on the right reflects the order (i.e., satisfies the condition `MulRightReflectLE`). For any elements $a, b, c \in \alpha$, if $a \cdot b = c \cdot b$, then $a = c$.

mul_le_mul_iff_of_ge theorem

 [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :
  a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Full source

@[to_additive] lemma mul_le_mul_iff_of_ge [MulLeftStrictMono α]
    [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :
    a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂ := by
  haveI := mulLeftMono_of_mulLeftStrictMono α
  haveI := mulRightMono_of_mulRightStrictMono α
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, ha, hb, true_and]
  refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
  exacts [mul_lt_mul_of_lt_of_le ha hb, mul_lt_mul_of_le_of_lt ha hb]

Strictly Monotone Multiplication Preserves Inequality: $a_2 \cdot b_2 \leq a_1 \cdot b_1 \leftrightarrow a_1 = a_2 \land b_1 = b_2$ under $a_1 \leq a_2$ and $b_1 \leq b_2$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). For any elements $a_1, a_2, b_1, b_2 \in \alpha$ with $a_1 \leq a_2$ and $b_1 \leq b_2$, we have $a_2 \cdot b_2 \leq a_1 \cdot b_1$ if and only if $a_1 = a_2$ and $b_1 = b_2$.

mul_eq_mul_iff_eq_and_eq theorem

 [MulLeftStrictMono α] [MulRightStrictMono α] {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) : a * b = c * d ↔ a = c ∧ b = d

Full source

@[to_additive] theorem mul_eq_mul_iff_eq_and_eq [MulLeftStrictMono α]
    [MulRightStrictMono α] {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) :
    a * b = c * d ↔ a = c ∧ b = d := by
  haveI := mulLeftMono_of_mulLeftStrictMono α
  haveI := mulRightMono_of_mulRightStrictMono α
  rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

Equality of Products under Monotonicity: $a \cdot b = c \cdot d \leftrightarrow a = c \land b = d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). For any elements $a, b, c, d \in \alpha$ with $a \leq c$ and $b \leq d$, we have $a \cdot b = c \cdot d$ if and only if $a = c$ and $b = d$.

mul_left_inj_of_comparable theorem

[MulRightStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) : c * a = b * a ↔ c = b

Full source

@[to_additive]
lemma mul_left_inj_of_comparable [MulRightStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) :
    c * a = b * a ↔ c = b := by
  refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_right' (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_right' (h.lt_of_ne h') a |>.ne

Left Cancellation of Multiplication under Comparability and Right Strict Monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order. If multiplication on the right is strictly monotone (i.e., the function $x \mapsto x * a$ is strictly increasing for any fixed $a$), then for any elements $a, b, c \in \alpha$ where $b$ and $c$ are comparable (i.e., $b \leq c$ or $c \leq b$), we have $c * a = b * a$ if and only if $c = b$.

mul_right_inj_of_comparable theorem

[MulLeftStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) : a * c = a * b ↔ c = b

Full source

@[to_additive]
lemma mul_right_inj_of_comparable [MulLeftStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) :
    a * c = a * b ↔ c = b := by
  refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_left' (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_left' (h.lt_of_ne h') a |>.ne

Right Cancellation of Multiplication under Comparability and Left Strict Monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order. If multiplication on the left is strictly monotone (i.e., the function $x \mapsto a * x$ is strictly increasing for any fixed $a$), then for any elements $a, b, c \in \alpha$ where $b$ and $c$ are comparable (i.e., $b \leq c$ or $c \leq b$), we have $a * c = a * b$ if and only if $c = b$.

trichotomy_of_mul_eq_mul theorem

[MulLeftStrictMono α] [MulRightStrictMono α] (h : a * b = c * d) : (a = c ∧ b = d) ∨ a < c ∨ b < d

Full source

@[to_additive]
theorem trichotomy_of_mul_eq_mul
    [MulLeftStrictMono α] [MulRightStrictMono α]
    (h : a * b = c * d) : (a = c ∧ b = d) ∨ a < c ∨ b < d := by
  obtain hac | rfl | hca := lt_trichotomy a c
  · right; left; exact hac
  · left; simpa using mul_right_inj_of_comparable (LinearOrder.le_total d b)|>.1 h
  · obtain hbd | rfl | hdb := lt_trichotomy b d
    · right; right; exact hbd
    · exact False.elim <| ne_of_lt (mul_lt_mul_right' hca b) h.symm
    · exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

Trichotomy for Products under Strictly-Monotone Multiplication: $a \cdot b = c \cdot d \implies (a = c \land b = d) \lor a < c \lor b < d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order such that multiplication is both left-strictly-monotone and right-strictly-monotone. For any elements $a, b, c, d \in \alpha$ satisfying $a \cdot b = c \cdot d$, exactly one of the following holds: 1. $a = c$ and $b = d$, or 2. $a < c$, or 3. $b < d$.

mul_max theorem

[CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : a * max b c = max (a * b) (a * c)

Full source

@[to_additive]
lemma mul_max [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
    a * max b c = max (a * b) (a * c) := mul_left_mono.map_max

Left Multiplication Distributes Over Maximum: $a \cdot \max(b, c) = \max(a \cdot b, a \cdot c)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c \in \alpha$, we have $a \cdot \max(b, c) = \max(a \cdot b, a \cdot c)$.

max_mul theorem

[CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) : max a b * c = max (a * c) (b * c)

Full source

@[to_additive]
lemma max_mul [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) :
    max a b * c = max (a * c) (b * c) := mul_right_mono.map_max

Maximum Distributes over Right Multiplication: $\max(a, b) * c = \max(a * c, b * c)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication on the right is monotone (i.e., for any fixed $c \in \alpha$, the function $x \mapsto x * c$ is monotone). Then for any elements $a, b, c \in \alpha$, we have $\max(a, b) * c = \max(a * c, b * c)$.

mul_min theorem

[CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : a * min b c = min (a * b) (a * c)

Full source

@[to_additive]
lemma mul_min [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
    a * min b c = min (a * b) (a * c) := mul_left_mono.map_min

Left Multiplication Distributes Over Minimum: $a \cdot \min(b, c) = \min(a \cdot b, a \cdot c)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c \in \alpha$, we have $a \cdot \min(b, c) = \min(a \cdot b, a \cdot c)$.

min_mul theorem

[CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) : min a b * c = min (a * c) (b * c)

Full source

@[to_additive]
lemma min_mul [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) :
    min a b * c = min (a * c) (b * c) := mul_right_mono.map_min

Minimum Distributes over Right Multiplication: $\min(a, b) * c = \min(a * c, b * c)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that right multiplication is monotone (i.e., for any fixed $c \in \alpha$, the function $x \mapsto x * c$ is monotone). Then for any elements $a, b, c \in \alpha$, the minimum of $a$ and $b$ multiplied by $c$ is equal to the minimum of $a * c$ and $b * c$, i.e., $\min(a, b) * c = \min(a * c, b * c)$.

min_lt_max_of_mul_lt_mul theorem

[MulLeftMono α] [MulRightMono α] (h : a * b < c * d) : min a b < max c d

Full source

@[to_additive] lemma min_lt_max_of_mul_lt_mul
    [MulLeftMono α] [MulRightMono α]
    (h : a * b < c * d) : min a b < max c d := by
  simp_rw [min_lt_iff, lt_max_iff]; contrapose! h; exact mul_le_mul' h.1.1 h.2.2

Minimum-Maximum Inequality from Strict Multiplication Order: $\min(a,b) < \max(c,d)$ when $a \cdot b < c \cdot d$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a \cdot b < c \cdot d$, we have $\min(a, b) < \max(c, d)$.

Left.min_le_max_of_mul_le_mul theorem

[MulLeftStrictMono α] [MulRightMono α] (h : a * b ≤ c * d) : min a b ≤ max c d

Full source

@[to_additive] lemma Left.min_le_max_of_mul_le_mul
    [MulLeftStrictMono α] [MulRightMono α]
    (h : a * b ≤ c * d) : min a b ≤ max c d := by
  simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

Minimum-Maximum Inequality under Left-Strictly-Monotone and Right-Monotone Multiplication: $a \cdot b \leq c \cdot d \implies \min(a, b) \leq \max(c, d)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a \cdot b \leq c \cdot d$, we have $\min(a, b) \leq \max(c, d)$.

Right.min_le_max_of_mul_le_mul theorem

[MulLeftMono α] [MulRightStrictMono α] (h : a * b ≤ c * d) : min a b ≤ max c d

Full source

@[to_additive] lemma Right.min_le_max_of_mul_le_mul
    [MulLeftMono α] [MulRightStrictMono α]
    (h : a * b ≤ c * d) : min a b ≤ max c d := by
  simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

Minimum-Maximum Inequality under Right-Strictly-Monotone Multiplication: $a \cdot b \leq c \cdot d \implies \min(a, b) \leq \max(c, d)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a \cdot b \leq c \cdot d$, we have $\min(a, b) \leq \max(c, d)$.

min_le_max_of_mul_le_mul theorem

[MulLeftStrictMono α] [MulRightStrictMono α] (h : a * b ≤ c * d) : min a b ≤ max c d

Full source

@[to_additive] lemma min_le_max_of_mul_le_mul
    [MulLeftStrictMono α] [MulRightStrictMono α]
    (h : a * b ≤ c * d) : min a b ≤ max c d :=
  haveI := mulRightMono_of_mulRightStrictMono α
  Left.min_le_max_of_mul_le_mul h

Minimum-Maximum Inequality under Strictly Monotone Multiplication: $a \cdot b \leq c \cdot d \implies \min(a, b) \leq \max(c, d)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). Then for any elements $a, b, c, d \in \alpha$ with $a \cdot b \leq c \cdot d$, we have $\min(a, b) \leq \max(c, d)$.

MulLeftStrictMono.toIsLeftCancelMul theorem

[MulLeftStrictMono α] : IsLeftCancelMul α

Full source

/-- Not an instance, to avoid loops with `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono`. -/
@[to_additive]
theorem MulLeftStrictMono.toIsLeftCancelMul [MulLeftStrictMono α] : IsLeftCancelMul α where
  mul_left_cancel _ _ _ h := mul_left_strictMono.injective h

Strictly monotone left multiplication implies left cancellation

Informal description

If multiplication on the left in a type $\alpha$ is strictly monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$), then $\alpha$ is left cancellative (i.e., $a \cdot b = a \cdot c$ implies $b = c$).

MulRightStrictMono.toIsRightCancelMul theorem

[MulRightStrictMono α] : IsRightCancelMul α

Full source

/-- Not an instance, to avoid loops with `IsRightCancelMul.mulRightStrictMono_of_mulRightMono`. -/
@[to_additive]
theorem MulRightStrictMono.toIsRightCancelMul [MulRightStrictMono α] : IsRightCancelMul α where
  mul_right_cancel _ _ _ h := mul_right_strictMono.injective h

Right Strictly Monotone Multiplication Implies Right Cancellativity

Informal description

If multiplication on the right is strictly monotone in a type $\alpha$ (i.e., the function $x \mapsto x \cdot a$ is strictly increasing for any fixed $a \in \alpha$), then the multiplication operation is right cancellative. That is, for any $a, b, c \in \alpha$, if $a \cdot c = b \cdot c$, then $a = b$.

max_mul_mul_le_max_mul_max' theorem

: max (a * b) (c * d) ≤ max a c * max b d

Full source

@[to_additive max_add_add_le_max_add_max]
theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
  max_le (mul_le_mul' (le_max_left _ _) <| le_max_left _ _) <|
    mul_le_mul' (le_max_right _ _) <| le_max_right _ _

Inequality for Maximum of Products: $\max(ab, cd) \leq \max(a, c) \cdot \max(b, d)$

Informal description

For any elements $a, b, c, d$ in a type $\alpha$ with a multiplication operation and a linear order, the maximum of the products $a \cdot b$ and $c \cdot d$ is less than or equal to the product of the maxima $\max(a, c) \cdot \max(b, d)$.

min_mul_min_le_min_mul_mul' theorem

: min a c * min b d ≤ min (a * b) (c * d)

Full source

@[to_additive min_add_min_le_min_add_add]
theorem min_mul_min_le_min_mul_mul' : min a c * min b d ≤ min (a * b) (c * d) :=
  le_min (mul_le_mul' (min_le_left _ _) <| min_le_left _ _) <|
    mul_le_mul' (min_le_right _ _) <| min_le_right _ _

Inequality for Products of Minima: $\min(a, c) \cdot \min(b, d) \leq \min(a \cdot b, c \cdot d)$

Informal description

For any elements $a, b, c, d$ in a linearly ordered type $\alpha$ with a multiplication operation, the product of the minima $\min(a, c) \cdot \min(b, d)$ is less than or equal to the minimum of the products $\min(a \cdot b, c \cdot d)$.

le_mul_of_one_le_right' theorem

[MulLeftMono α] {a b : α} (h : 1 ≤ b) : a ≤ a * b

Full source

@[to_additive le_add_of_nonneg_right]
theorem le_mul_of_one_le_right' [MulLeftMono α] {a b : α} (h : 1 ≤ b) :
    a ≤ a * b :=
  calc
    a = a * 1 := (mul_one a).symm
    _ ≤ a * b := mul_le_mul_left' h a

Right multiplication by element greater than or equal to one preserves order in left-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any element $a \in \alpha$ and any element $b \in \alpha$ satisfying $1 \leq b$, we have $a \leq a \cdot b$.

mul_le_of_le_one_right' theorem

[MulLeftMono α] {a b : α} (h : b ≤ 1) : a * b ≤ a

Full source

@[to_additive add_le_of_nonpos_right]
theorem mul_le_of_le_one_right' [MulLeftMono α] {a b : α} (h : b ≤ 1) :
    a * b ≤ a :=
  calc
    a * b ≤ a * 1 := mul_le_mul_left' h a
    _ = a := mul_one a

Right multiplication by element less than or equal to one preserves order in left-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b \in \alpha$ with $b \leq 1$, we have $a \cdot b \leq a$.

le_mul_of_one_le_left' theorem

[MulRightMono α] {a b : α} (h : 1 ≤ b) : a ≤ b * a

Full source

@[to_additive le_add_of_nonneg_left]
theorem le_mul_of_one_le_left' [MulRightMono α] {a b : α} (h : 1 ≤ b) :
    a ≤ b * a :=
  calc
    a = 1 * a := (one_mul a).symm
    _ ≤ b * a := mul_le_mul_right' h a

Left multiplication by element greater than or equal to one preserves order in right-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any element $a \in \alpha$ and any element $b \in \alpha$ satisfying $1 \leq b$, we have $a \leq b \cdot a$.

mul_le_of_le_one_left' theorem

[MulRightMono α] {a b : α} (h : b ≤ 1) : b * a ≤ a

Full source

@[to_additive add_le_of_nonpos_left]
theorem mul_le_of_le_one_left' [MulRightMono α] {a b : α} (h : b ≤ 1) :
    b * a ≤ a :=
  calc
    b * a ≤ 1 * a := mul_le_mul_right' h a
    _ = a := one_mul a

Right multiplication by element less than or equal to one preserves order in right-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b \in \alpha$ with $b \leq 1$, we have $b \cdot a \leq a$.

one_le_of_le_mul_right theorem

[MulLeftReflectLE α] {a b : α} (h : a ≤ a * b) : 1 ≤ b

Full source

@[to_additive]
theorem one_le_of_le_mul_right [MulLeftReflectLE α] {a b : α} (h : a ≤ a * b) :
    1 ≤ b :=
  le_of_mul_le_mul_left' (a := a) <| by simpa only [mul_one]

Right Multiplication Reflects Order: $a \leq a \cdot b \implies 1 \leq b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication on the left reflects the order (i.e., satisfies the condition `MulLeftReflectLE`). For any elements $a, b \in \alpha$, if $a \leq a \cdot b$, then $1 \leq b$.

le_one_of_mul_le_right theorem

[MulLeftReflectLE α] {a b : α} (h : a * b ≤ a) : b ≤ 1

Full source

@[to_additive]
theorem le_one_of_mul_le_right [MulLeftReflectLE α] {a b : α} (h : a * b ≤ a) :
    b ≤ 1 :=
  le_of_mul_le_mul_left' (a := a) <| by simpa only [mul_one]

Right Multiplication Reflects Order: $a \cdot b \leq a \implies b \leq 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication on the left reflects the order (i.e., satisfies the condition `MulLeftReflectLE`). For any elements $a, b \in \alpha$, if $a \cdot b \leq a$, then $b \leq 1$.

one_le_of_le_mul_left theorem

[MulRightReflectLE α] {a b : α} (h : b ≤ a * b) : 1 ≤ a

Full source

@[to_additive]
theorem one_le_of_le_mul_left [MulRightReflectLE α] {a b : α}
    (h : b ≤ a * b) :
    1 ≤ a :=
  le_of_mul_le_mul_right' (a := b) <| by simpa only [one_mul]

Right Multiplication Reflects Order: $b \leq a \cdot b \implies 1 \leq a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication on the right reflects the order (i.e., satisfies the condition `MulRightReflectLE`). For any elements $a, b \in \alpha$, if $b \leq a \cdot b$, then $1 \leq a$.

le_one_of_mul_le_left theorem

[MulRightReflectLE α] {a b : α} (h : a * b ≤ b) : a ≤ 1

Full source

@[to_additive]
theorem le_one_of_mul_le_left [MulRightReflectLE α] {a b : α}
    (h : a * b ≤ b) :
    a ≤ 1 :=
  le_of_mul_le_mul_right' (a := b) <| by simpa only [one_mul]

Right Multiplication Reflects Order: $a \cdot b \leq b \implies a \leq 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication on the right reflects the order (i.e., satisfies the condition `MulRightReflectLE`). For any elements $a, b \in \alpha$, if $a \cdot b \leq b$, then $a \leq 1$.

le_mul_iff_one_le_right' theorem

[MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α} : a ≤ a * b ↔ 1 ≤ b

Full source

@[to_additive (attr := simp) le_add_iff_nonneg_right]
theorem le_mul_iff_one_le_right' [MulLeftMono α]
    [MulLeftReflectLE α] (a : α) {b : α} :
    a ≤ a * b ↔ 1 ≤ b :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_iff_left a)

Order Characterization via Right Multiplication: $a \leq a \cdot b \leftrightarrow 1 \leq b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that left multiplication is monotone and order-reflecting. Then for any element $a \in \alpha$ and any element $b \in \alpha$, we have the equivalence: \[ a \leq a \cdot b \leftrightarrow 1 \leq b. \]

le_mul_iff_one_le_left' theorem

[MulRightMono α] [MulRightReflectLE α] (a : α) {b : α} : a ≤ b * a ↔ 1 ≤ b

Full source

@[to_additive (attr := simp) le_add_iff_nonneg_left]
theorem le_mul_iff_one_le_left' [MulRightMono α]
    [MulRightReflectLE α] (a : α) {b : α} :
    a ≤ b * a ↔ 1 ≤ b :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_iff_right a)

Order Characterization via Left Multiplication: $a \leq b \cdot a \leftrightarrow 1 \leq b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that right multiplication is monotone and order-reflecting. Then for any element $a \in \alpha$ and any element $b \in \alpha$, we have the equivalence: \[ a \leq b \cdot a \leftrightarrow 1 \leq b. \]

mul_le_iff_le_one_right' theorem

[MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α} : a * b ≤ a ↔ b ≤ 1

Full source

@[to_additive (attr := simp) add_le_iff_nonpos_right]
theorem mul_le_iff_le_one_right' [MulLeftMono α]
    [MulLeftReflectLE α] (a : α) {b : α} :
    a * b ≤ a ↔ b ≤ 1 :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_iff_left a)

Right Multiplication Below Identity: $a \cdot b \leq a \leftrightarrow b \leq 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that left multiplication is monotone and order-reflecting. Then for any element $a \in \alpha$ and any element $b \in \alpha$, we have the equivalence: \[ a \cdot b \leq a \leftrightarrow b \leq 1. \]

mul_le_iff_le_one_left' theorem

[MulRightMono α] [MulRightReflectLE α] {a b : α} : a * b ≤ b ↔ a ≤ 1

Full source

@[to_additive (attr := simp) add_le_iff_nonpos_left]
theorem mul_le_iff_le_one_left' [MulRightMono α]
    [MulRightReflectLE α] {a b : α} :
    a * b ≤ b ↔ a ≤ 1 :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_iff_right b)

Left Multiplication by $a$ is Below Identity iff $a \leq 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication is monotone and order-reflecting in the right argument. Then for any elements $a, b \in \alpha$, we have the equivalence: \[ a \cdot b \leq b \leftrightarrow a \leq 1. \]

lt_mul_of_one_lt_right' theorem

[MulLeftStrictMono α] (a : α) {b : α} (h : 1 < b) : a < a * b

Full source

@[to_additive lt_add_of_pos_right]
theorem lt_mul_of_one_lt_right' [MulLeftStrictMono α] (a : α) {b : α} (h : 1 < b) :
    a < a * b :=
  calc
    a = a * 1 := (mul_one a).symm
    _ < a * b := mul_lt_mul_left' h a

Strict inequality under right multiplication by an element greater than one

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone. For any element $a \in \alpha$ and any element $b \in \alpha$ such that $1 < b$, we have $a < a \cdot b$.

mul_lt_of_lt_one_right' theorem

[MulLeftStrictMono α] (a : α) {b : α} (h : b < 1) : a * b < a

Full source

@[to_additive add_lt_of_neg_right]
theorem mul_lt_of_lt_one_right' [MulLeftStrictMono α] (a : α) {b : α} (h : b < 1) :
    a * b < a :=
  calc
    a * b < a * 1 := mul_lt_mul_left' h a
    _ = a := mul_one a

Left multiplication by an element less than one decreases the value

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone. For any element $a \in \alpha$ and any element $b \in \alpha$ such that $b < 1$, we have $a \cdot b < a$.

lt_mul_of_one_lt_left' theorem

[MulRightStrictMono α] (a : α) {b : α} (h : 1 < b) : a < b * a

Full source

@[to_additive lt_add_of_pos_left]
theorem lt_mul_of_one_lt_left' [MulRightStrictMono α] (a : α) {b : α}
    (h : 1 < b) :
    a < b * a :=
  calc
    a = 1 * a := (one_mul a).symm
    _ < b * a := mul_lt_mul_right' h a

Right multiplication by an element greater than one increases the value

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where right multiplication is strictly monotone. For any element $a \in \alpha$ and any element $b \in \alpha$ such that $1 < b$, we have $a < b \cdot a$.

mul_lt_of_lt_one_left' theorem

[MulRightStrictMono α] (a : α) {b : α} (h : b < 1) : b * a < a

Full source

@[to_additive add_lt_of_neg_left]
theorem mul_lt_of_lt_one_left' [MulRightStrictMono α] (a : α) {b : α}
    (h : b < 1) :
    b * a < a :=
  calc
    b * a < 1 * a := mul_lt_mul_right' h a
    _ = a := one_mul a

Right multiplication by an element less than one decreases the value

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where right multiplication is strictly monotone. For any element $a \in \alpha$ and any element $b \in \alpha$ such that $b < 1$, we have $b \cdot a < a$.

one_lt_of_lt_mul_right theorem

[MulLeftReflectLT α] {a b : α} (h : a < a * b) : 1 < b

Full source

@[to_additive]
theorem one_lt_of_lt_mul_right [MulLeftReflectLT α] {a b : α} (h : a < a * b) :
    1 < b :=
  lt_of_mul_lt_mul_left' (a := a) <| by simpa only [mul_one]

Left Multiplication Reflects Strict Order: $a < a \cdot b \to 1 < b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication on the left reflects the strict order (i.e., $a \cdot b < a \cdot c$ implies $b < c$). Then for any elements $a, b \in \alpha$, if $a < a \cdot b$, it follows that $1 < b$.

lt_one_of_mul_lt_right theorem

[MulLeftReflectLT α] {a b : α} (h : a * b < a) : b < 1

Full source

@[to_additive]
theorem lt_one_of_mul_lt_right [MulLeftReflectLT α] {a b : α} (h : a * b < a) :
    b < 1 :=
  lt_of_mul_lt_mul_left' (a := a) <| by simpa only [mul_one]

Left Multiplication Reflects Strict Order: $a * b < a \to b < 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication on the left reflects the strict order (i.e., $a * b < a * c$ implies $b < c$). Then for any elements $a, b \in \alpha$, if $a * b < a$, it follows that $b < 1$.

one_lt_of_lt_mul_left theorem

[MulRightReflectLT α] {a b : α} (h : b < a * b) : 1 < a

Full source

@[to_additive]
theorem one_lt_of_lt_mul_left [MulRightReflectLT α] {a b : α}
    (h : b < a * b) :
    1 < a :=
  lt_of_mul_lt_mul_right' (a := b) <| by simpa only [one_mul]

Right Multiplication Reflects Strict Order: $b < a \cdot b \to 1 < a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication on the right reflects the strict order (i.e., $b < a * b$ implies $1 < a$). Then for any elements $a, b \in \alpha$, if $b < a * b$, it follows that $1 < a$.

lt_one_of_mul_lt_left theorem

[MulRightReflectLT α] {a b : α} (h : a * b < b) : a < 1

Full source

@[to_additive]
theorem lt_one_of_mul_lt_left [MulRightReflectLT α] {a b : α}
    (h : a * b < b) :
    a < 1 :=
  lt_of_mul_lt_mul_right' (a := b) <| by simpa only [one_mul]

Left Multiplication Reflects Strict Order: $a \cdot b < b \to a < 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication on the right reflects the strict order (i.e., $a * b < c * b$ implies $a < c$). Then for any elements $a, b \in \alpha$, if $a * b < b$, it follows that $a < 1$.

lt_mul_iff_one_lt_right' theorem

[MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b : α} : a < a * b ↔ 1 < b

Full source

@[to_additive (attr := simp) lt_add_iff_pos_right]
theorem lt_mul_iff_one_lt_right' [MulLeftStrictMono α]
    [MulLeftReflectLT α] (a : α) {b : α} :
    a < a * b ↔ 1 < b :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_iff_left a)

Strict Left Multiplication Order Criterion: $a < a \cdot b \leftrightarrow 1 < b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict partial order, such that multiplication is strictly monotone in the left argument and reflects the strict order in the left argument. Then for any element $a \in \alpha$ and any element $b \in \alpha$, we have $a < a \cdot b$ if and only if $1 < b$.

lt_mul_iff_one_lt_left' theorem

[MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b : α} : a < b * a ↔ 1 < b

Full source

@[to_additive (attr := simp) lt_add_iff_pos_left]
theorem lt_mul_iff_one_lt_left' [MulRightStrictMono α]
    [MulRightReflectLT α] (a : α) {b : α} : a < b * a ↔ 1 < b :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_iff_right a)

Strict Right Multiplication Order Criterion: $a < b \cdot a \leftrightarrow 1 < b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication is strictly monotone and reflects the strict order in the right argument. Then for any elements $a, b \in \alpha$, we have $a < b \cdot a$ if and only if $1 < b$.

mul_lt_iff_lt_one_left' theorem

[MulLeftStrictMono α] [MulLeftReflectLT α] {a b : α} : a * b < a ↔ b < 1

Full source

@[to_additive (attr := simp) add_lt_iff_neg_left]
theorem mul_lt_iff_lt_one_left' [MulLeftStrictMono α]
    [MulLeftReflectLT α] {a b : α} :
    a * b < a ↔ b < 1 :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_iff_left a)

Left Multiplication Order Criterion: $a \cdot b < a \leftrightarrow b < 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict partial order, such that multiplication is strictly monotone in the left argument and reflects the strict order in the left argument. Then for any elements $a, b \in \alpha$, we have $a \cdot b < a$ if and only if $b < 1$.

mul_lt_iff_lt_one_right' theorem

[MulRightStrictMono α] [MulRightReflectLT α] {a : α} (b : α) : a * b < b ↔ a < 1

Full source

@[to_additive (attr := simp) add_lt_iff_neg_right]
theorem mul_lt_iff_lt_one_right' [MulRightStrictMono α]
    [MulRightReflectLT α] {a : α} (b : α) : a * b < b ↔ a < 1 :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_iff_right b)

Right Multiplication Order Criterion: $a \cdot b < b \leftrightarrow a < 1$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, such that multiplication is strictly monotone in the right argument and reflects the strict order in the right argument. Then for any elements $a, b \in \alpha$, we have $a \cdot b < b$ if and only if $a < 1$.

mul_le_of_le_of_le_one theorem

[MulLeftMono α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c

Full source

@[to_additive]
theorem mul_le_of_le_of_le_one [MulLeftMono α] {a b c : α} (hbc : b ≤ c)
    (ha : a ≤ 1) :
    b * a ≤ c :=
  calc
    b * a ≤ b * 1 := mul_le_mul_left' ha b
    _ = b := mul_one b
    _ ≤ c := hbc

Left multiplication by an element less than or equal to one preserves order

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $b, c \in \alpha$ with $b \leq c$, and any element $a \in \alpha$ with $a \leq 1$, we have $b \cdot a \leq c$.

mul_lt_of_le_of_lt_one theorem

[MulLeftStrictMono α] {a b c : α} (hbc : b ≤ c) (ha : a < 1) : b * a < c

Full source

@[to_additive]
theorem mul_lt_of_le_of_lt_one [MulLeftStrictMono α] {a b c : α} (hbc : b ≤ c)
    (ha : a < 1) :
    b * a < c :=
  calc
    b * a < b * 1 := mul_lt_mul_left' ha b
    _ = b := mul_one b
    _ ≤ c := hbc

Strict inequality under left multiplication with element less than one: $b \leq c \land a < 1 \implies b \cdot a < c$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, where left multiplication is strictly monotone. For any elements $a, b, c \in \alpha$, if $b \leq c$ and $a < 1$, then $b \cdot a < c$.

mul_lt_of_lt_of_le_one theorem

[MulLeftMono α] {a b c : α} (hbc : b < c) (ha : a ≤ 1) : b * a < c

Full source

@[to_additive]
theorem mul_lt_of_lt_of_le_one [MulLeftMono α] {a b c : α} (hbc : b < c)
    (ha : a ≤ 1) :
    b * a < c :=
  calc
    b * a ≤ b * 1 := mul_le_mul_left' ha b
    _ = b := mul_one b
    _ < c := hbc

Strict Inequality Preservation Under Left Multiplication with Unit Factor

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $b, c \in \alpha$ with $b < c$, and any element $a \in \alpha$ with $a \leq 1$, we have $b \cdot a < c$.

mul_lt_of_lt_of_lt_one theorem

[MulLeftStrictMono α] {a b c : α} (hbc : b < c) (ha : a < 1) : b * a < c

Full source

@[to_additive]
theorem mul_lt_of_lt_of_lt_one [MulLeftStrictMono α] {a b c : α} (hbc : b < c)
    (ha : a < 1) :
    b * a < c :=
  calc
    b * a < b * 1 := mul_lt_mul_left' ha b
    _ = b := mul_one b
    _ < c := hbc

Strict Inequality Preservation Under Left Multiplication with Unit Factor

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone. For any elements $a, b, c \in \alpha$ such that $b < c$ and $a < 1$, we have $b \cdot a < c$.

mul_lt_of_lt_of_lt_one' theorem

[MulLeftMono α] {a b c : α} (hbc : b < c) (ha : a < 1) : b * a < c

Full source

@[to_additive]
theorem mul_lt_of_lt_of_lt_one' [MulLeftMono α] {a b c : α} (hbc : b < c)
    (ha : a < 1) :
    b * a < c :=
  mul_lt_of_lt_of_le_one hbc ha.le

Strict Inequality Preservation Under Left Multiplication with Subunit Factor

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $b, c \in \alpha$ with $b < c$, and any element $a \in \alpha$ with $a < 1$, we have $b \cdot a < c$.

Left.mul_le_one theorem

[MulLeftMono α] {a b : α} (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_le_one`. -/
@[to_additive "Assumes left covariance.
The lemma assuming right covariance is `Right.add_nonpos`."]
theorem Left.mul_le_one [MulLeftMono α] {a b : α} (ha : a ≤ 1) (hb : b ≤ 1) :
    a * b ≤ 1 :=
  mul_le_of_le_of_le_one ha hb

Left Multiplication of Elements Less Than or Equal to One Yields Result Less Than or Equal to One

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b \in \alpha$ with $a \leq 1$ and $b \leq 1$, we have $a \cdot b \leq 1$.

Left.mul_lt_one_of_le_of_lt theorem

[MulLeftStrictMono α] {a b : α} (ha : a ≤ 1) (hb : b < 1) : a * b < 1

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one_of_le_of_lt`. -/
@[to_additive Left.add_neg_of_nonpos_of_neg
      "Assumes left covariance.
      The lemma assuming right covariance is `Right.add_neg_of_nonpos_of_neg`."]
theorem Left.mul_lt_one_of_le_of_lt [MulLeftStrictMono α] {a b : α} (ha : a ≤ 1)
    (hb : b < 1) :
    a * b < 1 :=
  mul_lt_of_le_of_lt_one ha hb

Strict Inequality Under Left Multiplication with One Element Less Than or Equal to One and Another Less Than One

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order, where left multiplication is strictly monotone. For any elements $a, b \in \alpha$, if $a \leq 1$ and $b < 1$, then $a \cdot b < 1$.

Left.mul_lt_one_of_lt_of_le theorem

[MulLeftMono α] {a b : α} (ha : a < 1) (hb : b ≤ 1) : a * b < 1

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one_of_lt_of_le`. -/
@[to_additive Left.add_neg_of_neg_of_nonpos
      "Assumes left covariance.
      The lemma assuming right covariance is `Right.add_neg_of_neg_of_nonpos`."]
theorem Left.mul_lt_one_of_lt_of_le [MulLeftMono α] {a b : α} (ha : a < 1)
    (hb : b ≤ 1) :
    a * b < 1 :=
  mul_lt_of_lt_of_le_one ha hb

Left Multiplication of Strictly Less Than One and Less Than or Equal to One Yields Result Strictly Less Than One

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b \in \alpha$ with $a < 1$ and $b \leq 1$, we have $a \cdot b < 1$.

Left.mul_lt_one theorem

[MulLeftStrictMono α] {a b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one`. -/
@[to_additive "Assumes left covariance.
The lemma assuming right covariance is `Right.add_neg`."]
theorem Left.mul_lt_one [MulLeftStrictMono α] {a b : α} (ha : a < 1) (hb : b < 1) :
    a * b < 1 :=
  mul_lt_of_lt_of_lt_one ha hb

Strict Inequality Preservation Under Multiplication of Two Elements Less Than One

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone. For any elements $a, b \in \alpha$ such that $a < 1$ and $b < 1$, we have $a \cdot b < 1$.

Left.mul_lt_one' theorem

[MulLeftMono α] {a b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one'`. -/
@[to_additive "Assumes left covariance.
The lemma assuming right covariance is `Right.add_neg'`."]
theorem Left.mul_lt_one' [MulLeftMono α] {a b : α} (ha : a < 1) (hb : b < 1) :
    a * b < 1 :=
  mul_lt_of_lt_of_lt_one' ha hb

Product of Two Elements Less Than One is Less Than One (Left-Monotone Case)

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b \in \alpha$ with $a < 1$ and $b < 1$, we have $a \cdot b < 1$.

le_mul_of_le_of_one_le theorem

[MulLeftMono α] {a b c : α} (hbc : b ≤ c) (ha : 1 ≤ a) : b ≤ c * a

Full source

@[to_additive]
theorem le_mul_of_le_of_one_le [MulLeftMono α] {a b c : α} (hbc : b ≤ c)
    (ha : 1 ≤ a) :
    b ≤ c * a :=
  calc
    b ≤ c := hbc
    _ = c * 1 := (mul_one c).symm
    _ ≤ c * a := mul_le_mul_left' ha c

Left-monotone multiplication preserves order with unit lower bound

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $b, c \in \alpha$ with $b \leq c$, and any element $a \in \alpha$ with $1 \leq a$, we have $b \leq c \cdot a$.

lt_mul_of_le_of_one_lt theorem

[MulLeftStrictMono α] {a b c : α} (hbc : b ≤ c) (ha : 1 < a) : b < c * a

Full source

@[to_additive]
theorem lt_mul_of_le_of_one_lt [MulLeftStrictMono α] {a b c : α} (hbc : b ≤ c)
    (ha : 1 < a) :
    b < c * a :=
  calc
    b ≤ c := hbc
    _ = c * 1 := (mul_one c).symm
    _ < c * a := mul_lt_mul_left' ha c

Strict inequality under left multiplication with unit greater than one: $b < c \cdot a$ when $b \leq c$ and $1 < a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that left multiplication is strictly monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$). Then for any elements $b, c \in \alpha$ with $b \leq c$, and any element $a \in \alpha$ with $1 < a$, we have $b < c \cdot a$.

lt_mul_of_lt_of_one_le theorem

[MulLeftMono α] {a b c : α} (hbc : b < c) (ha : 1 ≤ a) : b < c * a

Full source

@[to_additive]
theorem lt_mul_of_lt_of_one_le [MulLeftMono α] {a b c : α} (hbc : b < c)
    (ha : 1 ≤ a) :
    b < c * a :=
  calc
    b < c := hbc
    _ = c * 1 := (mul_one c).symm
    _ ≤ c * a := mul_le_mul_left' ha c

Strict inequality under left multiplication with unit lower bound: $b < c \cdot a$ when $b < c$ and $1 \leq a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $b, c \in \alpha$ with $b < c$, and any element $a \in \alpha$ with $1 \leq a$, we have $b < c \cdot a$.

lt_mul_of_lt_of_one_lt theorem

[MulLeftStrictMono α] {a b c : α} (hbc : b < c) (ha : 1 < a) : b < c * a

Full source

@[to_additive]
theorem lt_mul_of_lt_of_one_lt [MulLeftStrictMono α] {a b c : α} (hbc : b < c)
    (ha : 1 < a) :
    b < c * a :=
  calc
    b < c := hbc
    _ = c * 1 := (mul_one c).symm
    _ < c * a := mul_lt_mul_left' ha c

Strict inequality under left multiplication with unit greater than one: $b < c * a$ when $b < c$ and $1 < a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone. For any elements $a, b, c \in \alpha$, if $b < c$ and $1 < a$, then $b < c * a$.

lt_mul_of_lt_of_one_lt' theorem

[MulLeftMono α] {a b c : α} (hbc : b < c) (ha : 1 < a) : b < c * a

Full source

@[to_additive]
theorem lt_mul_of_lt_of_one_lt' [MulLeftMono α] {a b c : α} (hbc : b < c)
    (ha : 1 < a) :
    b < c * a :=
  lt_mul_of_lt_of_one_le hbc ha.le

Strict inequality under left multiplication with unit greater than one: $b < c \cdot a$ when $b < c$ and $1 < a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $b, c \in \alpha$ with $b < c$, and any element $a \in \alpha$ with $1 < a$, we have $b < c \cdot a$.

Left.one_le_mul theorem

[MulLeftMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_le_mul`. -/
@[to_additive Left.add_nonneg "Assumes left covariance.
The lemma assuming right covariance is `Right.add_nonneg`."]
theorem Left.one_le_mul [MulLeftMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
    1 ≤ a * b :=
  le_mul_of_le_of_one_le ha hb

Product of elements greater than or equal to one is greater than or equal to one under left-monotone multiplication

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b \in \alpha$ with $1 \leq a$ and $1 \leq b$, we have $1 \leq a \cdot b$.

Left.one_lt_mul_of_le_of_lt theorem

[MulLeftStrictMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul_of_le_of_lt`. -/
@[to_additive Left.add_pos_of_nonneg_of_pos
      "Assumes left covariance.
      The lemma assuming right covariance is `Right.add_pos_of_nonneg_of_pos`."]
theorem Left.one_lt_mul_of_le_of_lt [MulLeftStrictMono α] {a b : α} (ha : 1 ≤ a)
    (hb : 1 < b) :
    1 < a * b :=
  lt_mul_of_le_of_one_lt ha hb

Product of elements with one less than or equal and one strictly greater than one is strictly greater than one under left-strictly monotone multiplication

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that left multiplication is strictly monotone. For any elements $a, b \in \alpha$, if $1 \leq a$ and $1 < b$, then $1 < a \cdot b$.

Left.one_lt_mul_of_lt_of_le theorem

[MulLeftMono α] {a b : α} (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul_of_lt_of_le`. -/
@[to_additive Left.add_pos_of_pos_of_nonneg
      "Assumes left covariance.
      The lemma assuming right covariance is `Right.add_pos_of_pos_of_nonneg`."]
theorem Left.one_lt_mul_of_lt_of_le [MulLeftMono α] {a b : α} (ha : 1 < a)
    (hb : 1 ≤ b) :
    1 < a * b :=
  lt_mul_of_lt_of_one_le ha hb

Product of elements with one strictly less than $a$ and one less than or equal to $b$ is strictly greater than one under left-monotone multiplication

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b \in \alpha$ with $1 < a$ and $1 \leq b$, we have $1 < a \cdot b$.

Left.one_lt_mul theorem

[MulLeftStrictMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul`. -/
@[to_additive Left.add_pos "Assumes left covariance.
The lemma assuming right covariance is `Right.add_pos`."]
theorem Left.one_lt_mul [MulLeftStrictMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) :
    1 < a * b :=
  lt_mul_of_lt_of_one_lt ha hb

Product of elements greater than one is greater than one under left-strictly monotone multiplication

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone. For any elements $a, b \in \alpha$, if $1 < a$ and $1 < b$, then $1 < a * b$.

Left.one_lt_mul' theorem

[MulLeftMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

Full source

/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul'`. -/
@[to_additive Left.add_pos' "Assumes left covariance.
The lemma assuming right covariance is `Right.add_pos'`."]
theorem Left.one_lt_mul' [MulLeftMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) :
    1 < a * b :=
  lt_mul_of_lt_of_one_lt' ha hb

Product of elements greater than one is greater than one under left-monotone multiplication

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b \in \alpha$ with $1 < a$ and $1 < b$, we have $1 < a \cdot b$.

mul_le_of_le_one_of_le theorem

[MulRightMono α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c

Full source

@[to_additive]
theorem mul_le_of_le_one_of_le [MulRightMono α] {a b c : α} (ha : a ≤ 1)
    (hbc : b ≤ c) :
    a * b ≤ c :=
  calc
    a * b ≤ 1 * b := mul_le_mul_right' ha b
    _ = b := one_mul b
    _ ≤ c := hbc

Right multiplication by an element less than or equal to one preserves order

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone. For any elements $a, b, c \in \alpha$ with $a \leq 1$ and $b \leq c$, we have $a \cdot b \leq c$.

mul_lt_of_lt_one_of_le theorem

[MulRightStrictMono α] {a b c : α} (ha : a < 1) (hbc : b ≤ c) : a * b < c

Full source

@[to_additive]
theorem mul_lt_of_lt_one_of_le [MulRightStrictMono α] {a b c : α} (ha : a < 1)
    (hbc : b ≤ c) :
    a * b < c :=
  calc
    a * b < 1 * b := mul_lt_mul_right' ha b
    _ = b := one_mul b
    _ ≤ c := hbc

Strict inequality under right multiplication with element less than one and non-strict inequality

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where multiplication on the right is strictly monotone. For any elements $a, b, c \in \alpha$ such that $a < 1$ and $b \leq c$, it holds that $a \cdot b < c$.

mul_lt_of_le_one_of_lt theorem

[MulRightMono α] {a b c : α} (ha : a ≤ 1) (hb : b < c) : a * b < c

Full source

@[to_additive]
theorem mul_lt_of_le_one_of_lt [MulRightMono α] {a b c : α} (ha : a ≤ 1)
    (hb : b < c) :
    a * b < c :=
  calc
    a * b ≤ 1 * b := mul_le_mul_right' ha b
    _ = b := one_mul b
    _ < c := hb

Strict inequality under right multiplication with element at most one

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone. For any elements $a, b, c \in \alpha$ with $a \leq 1$ and $b < c$, we have $a \cdot b < c$.

mul_lt_of_lt_one_of_lt theorem

[MulRightStrictMono α] {a b c : α} (ha : a < 1) (hb : b < c) : a * b < c

Full source

@[to_additive]
theorem mul_lt_of_lt_one_of_lt [MulRightStrictMono α] {a b c : α} (ha : a < 1)
    (hb : b < c) :
    a * b < c :=
  calc
    a * b < 1 * b := mul_lt_mul_right' ha b
    _ = b := one_mul b
    _ < c := hb

Strict inequality under right multiplication with element less than one

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where multiplication on the right is strictly monotone. For any elements $a, b, c \in \alpha$ such that $a < 1$ and $b < c$, it holds that $a \cdot b < c$.

mul_lt_of_lt_one_of_lt' theorem

[MulRightMono α] {a b c : α} (ha : a < 1) (hbc : b < c) : a * b < c

Full source

@[to_additive]
theorem mul_lt_of_lt_one_of_lt' [MulRightMono α] {a b c : α} (ha : a < 1)
    (hbc : b < c) :
    a * b < c :=
  mul_lt_of_le_one_of_lt ha.le hbc

Strict inequality under right multiplication with element less than one (variant)

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone. For any elements $a, b, c \in \alpha$ with $a < 1$ and $b < c$, we have $a \cdot b < c$.

Right.mul_le_one theorem

[MulRightMono α] {a b : α} (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_le_one`. -/
@[to_additive "Assumes right covariance.
The lemma assuming left covariance is `Left.add_nonpos`."]
theorem Right.mul_le_one [MulRightMono α] {a b : α} (ha : a ≤ 1)
    (hb : b ≤ 1) :
    a * b ≤ 1 :=
  mul_le_of_le_one_of_le ha hb

Right multiplication of elements less than or equal to one is less than or equal to one

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone. For any elements $a, b \in \alpha$ with $a \leq 1$ and $b \leq 1$, we have $a \cdot b \leq 1$.

Right.mul_lt_one_of_lt_of_le theorem

[MulRightStrictMono α] {a b : α} (ha : a < 1) (hb : b ≤ 1) : a * b < 1

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one_of_lt_of_le`. -/
@[to_additive Right.add_neg_of_neg_of_nonpos
      "Assumes right covariance.
      The lemma assuming left covariance is `Left.add_neg_of_neg_of_nonpos`."]
theorem Right.mul_lt_one_of_lt_of_le [MulRightStrictMono α] {a b : α}
    (ha : a < 1) (hb : b ≤ 1) :
    a * b < 1 :=
  mul_lt_of_lt_one_of_le ha hb

Strict Inequality Under Right Multiplication with Element Less Than One and Non-Strict Inequality

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where multiplication on the right is strictly monotone. For any elements $a, b \in \alpha$ such that $a < 1$ and $b \leq 1$, it holds that $a \cdot b < 1$.

Right.mul_lt_one_of_le_of_lt theorem

[MulRightMono α] {a b : α} (ha : a ≤ 1) (hb : b < 1) : a * b < 1

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one_of_le_of_lt`. -/
@[to_additive Right.add_neg_of_nonpos_of_neg
      "Assumes right covariance.
      The lemma assuming left covariance is `Left.add_neg_of_nonpos_of_neg`."]
theorem Right.mul_lt_one_of_le_of_lt [MulRightMono α] {a b : α}
    (ha : a ≤ 1) (hb : b < 1) :
    a * b < 1 :=
  mul_lt_of_le_one_of_lt ha hb

Strict Inequality Under Right Multiplication with Element at Most One and Element Less Than One

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone. For any elements $a, b \in \alpha$ with $a \leq 1$ and $b < 1$, we have $a \cdot b < 1$.

Right.mul_lt_one theorem

[MulRightStrictMono α] {a b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one`. -/
@[to_additive "Assumes right covariance.
The lemma assuming left covariance is `Left.add_neg`."]
theorem Right.mul_lt_one [MulRightStrictMono α] {a b : α} (ha : a < 1)
    (hb : b < 1) :
    a * b < 1 :=
  mul_lt_of_lt_one_of_lt ha hb

Strict Inequality Under Right Multiplication of Elements Less Than One

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where multiplication on the right is strictly monotone. For any elements $a, b \in \alpha$ such that $a < 1$ and $b < 1$, it holds that $a \cdot b < 1$.

Right.mul_lt_one' theorem

[MulRightMono α] {a b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one'`. -/
@[to_additive "Assumes right covariance.
The lemma assuming left covariance is `Left.add_neg'`."]
theorem Right.mul_lt_one' [MulRightMono α] {a b : α} (ha : a < 1)
    (hb : b < 1) :
    a * b < 1 :=
  mul_lt_of_lt_one_of_lt' ha hb

Strict Inequality Under Right Multiplication of Elements Less Than One (Variant)

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone. For any elements $a, b \in \alpha$ with $a < 1$ and $b < 1$, we have $a \cdot b < 1$.

le_mul_of_one_le_of_le theorem

[MulRightMono α] {a b c : α} (ha : 1 ≤ a) (hbc : b ≤ c) : b ≤ a * c

Full source

@[to_additive]
theorem le_mul_of_one_le_of_le [MulRightMono α] {a b c : α} (ha : 1 ≤ a)
    (hbc : b ≤ c) :
    b ≤ a * c :=
  calc
    b ≤ c := hbc
    _ = 1 * c := (one_mul c).symm
    _ ≤ a * c := mul_le_mul_right' ha c

Right-monotone multiplication preserves order under unit condition

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b, c \in \alpha$ such that $1 \leq a$ and $b \leq c$, we have $b \leq a \cdot c$.

lt_mul_of_one_lt_of_le theorem

[MulRightStrictMono α] {a b c : α} (ha : 1 < a) (hbc : b ≤ c) : b < a * c

Full source

@[to_additive]
theorem lt_mul_of_one_lt_of_le [MulRightStrictMono α] {a b c : α} (ha : 1 < a)
    (hbc : b ≤ c) :
    b < a * c :=
  calc
    b ≤ c := hbc
    _ = 1 * c := (one_mul c).symm
    _ < a * c := mul_lt_mul_right' ha c

Strict inequality under right multiplication with a strictly greater-than-one element and non-strict inequality

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, such that multiplication on the right is strictly monotone. For any elements $a, b, c \in \alpha$, if $1 < a$ and $b \leq c$, then $b < a \cdot c$.

lt_mul_of_one_le_of_lt theorem

[MulRightMono α] {a b c : α} (ha : 1 ≤ a) (hbc : b < c) : b < a * c

Full source

@[to_additive]
theorem lt_mul_of_one_le_of_lt [MulRightMono α] {a b c : α} (ha : 1 ≤ a)
    (hbc : b < c) :
    b < a * c :=
  calc
    b < c := hbc
    _ = 1 * c := (one_mul c).symm
    _ ≤ a * c := mul_le_mul_right' ha c

Strict inequality under right multiplication with a greater-than-or-equal-to-one element

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b, c \in \alpha$ such that $1 \leq a$ and $b < c$, we have $b < a \cdot c$.

lt_mul_of_one_lt_of_lt theorem

[MulRightStrictMono α] {a b c : α} (ha : 1 < a) (hbc : b < c) : b < a * c

Full source

@[to_additive]
theorem lt_mul_of_one_lt_of_lt [MulRightStrictMono α] {a b c : α} (ha : 1 < a)
    (hbc : b < c) :
    b < a * c :=
  calc
    b < c := hbc
    _ = 1 * c := (one_mul c).symm
    _ < a * c := mul_lt_mul_right' ha c

Strict inequality under right multiplication with a strictly greater-than-one element

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, such that multiplication on the right is strictly monotone. For any elements $a, b, c \in \alpha$, if $1 < a$ and $b < c$, then $b < a * c$.

lt_mul_of_one_lt_of_lt' theorem

[MulRightMono α] {a b c : α} (ha : 1 < a) (hbc : b < c) : b < a * c

Full source

@[to_additive]
theorem lt_mul_of_one_lt_of_lt' [MulRightMono α] {a b c : α} (ha : 1 < a)
    (hbc : b < c) :
    b < a * c :=
  lt_mul_of_one_le_of_lt ha.le hbc

Strict inequality under right multiplication with a strictly greater-than-one element in right-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b, c \in \alpha$ such that $1 < a$ and $b < c$, we have $b < a \cdot c$.

Right.one_le_mul theorem

[MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_le_mul`. -/
@[to_additive Right.add_nonneg "Assumes right covariance.
The lemma assuming left covariance is `Left.add_nonneg`."]
theorem Right.one_le_mul [MulRightMono α] {a b : α} (ha : 1 ≤ a)
    (hb : 1 ≤ b) :
    1 ≤ a * b :=
  le_mul_of_one_le_of_le ha hb

Right-monotone multiplication preserves unit inequalities: $1 \leq a \cdot b$ when $1 \leq a$ and $1 \leq b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b \in \alpha$ such that $1 \leq a$ and $1 \leq b$, we have $1 \leq a \cdot b$.

Right.one_lt_mul_of_lt_of_le theorem

[MulRightStrictMono α] {a b : α} (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul_of_lt_of_le`. -/
@[to_additive Right.add_pos_of_pos_of_nonneg
"Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos_of_pos_of_nonneg`."]
theorem Right.one_lt_mul_of_lt_of_le [MulRightStrictMono α] {a b : α}
    (ha : 1 < a) (hb : 1 ≤ b) :
    1 < a * b :=
  lt_mul_of_one_lt_of_le ha hb

Right-monotone multiplication preserves strict inequality with unit: $1 < a \cdot b$ when $1 < a$ and $1 \leq b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, such that multiplication on the right is strictly monotone. For any elements $a, b \in \alpha$, if $1 < a$ and $1 \leq b$, then $1 < a \cdot b$.

Right.one_lt_mul_of_le_of_lt theorem

[MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul_of_le_of_lt`. -/
@[to_additive Right.add_pos_of_nonneg_of_pos
"Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos_of_nonneg_of_pos`."]
theorem Right.one_lt_mul_of_le_of_lt [MulRightMono α] {a b : α}
    (ha : 1 ≤ a) (hb : 1 < b) :
    1 < a * b :=
  lt_mul_of_one_le_of_lt ha hb

Product of elements with one less than or equal and one strictly greater than one is greater than one (right multiplicative version)

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b \in \alpha$ such that $1 \leq a$ and $1 < b$, we have $1 < a \cdot b$.

Right.one_lt_mul theorem

[MulRightStrictMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul`. -/
@[to_additive Right.add_pos "Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos`."]
theorem Right.one_lt_mul [MulRightStrictMono α] {a b : α} (ha : 1 < a)
    (hb : 1 < b) :
    1 < a * b :=
  lt_mul_of_one_lt_of_lt ha hb

Product of elements greater than one is greater than one (right multiplicative version)

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, such that multiplication on the right is strictly monotone. For any elements $a, b \in \alpha$, if $1 < a$ and $1 < b$, then $1 < a * b$.

Right.one_lt_mul' theorem

[MulRightMono α] {a b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

Full source

/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul'`. -/
@[to_additive Right.add_pos' "Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos'`."]
theorem Right.one_lt_mul' [MulRightMono α] {a b : α} (ha : 1 < a)
    (hb : 1 < b) :
    1 < a * b :=
  lt_mul_of_one_lt_of_lt' ha hb

Product of elements greater than one is greater than one (right multiplicative version)

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b \in \alpha$ such that $1 < a$ and $1 < b$, we have $1 < a \cdot b$.

lt_of_mul_lt_of_one_le_left theorem

[MulLeftMono α] {a b c : α} (h : a * b < c) (hle : 1 ≤ b) : a < c

Full source

@[to_additive]
theorem lt_of_mul_lt_of_one_le_left [MulLeftMono α] {a b c : α} (h : a * b < c)
    (hle : 1 ≤ b) :
    a < c :=
  (le_mul_of_one_le_right' hle).trans_lt h

Left multiplication preserves strict inequality when right factor is at least one

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b, c \in \alpha$, if $a \cdot b < c$ and $1 \leq b$, then $a < c$.

le_of_mul_le_of_one_le_left theorem

[MulLeftMono α] {a b c : α} (h : a * b ≤ c) (hle : 1 ≤ b) : a ≤ c

Full source

@[to_additive]
theorem le_of_mul_le_of_one_le_left [MulLeftMono α] {a b c : α} (h : a * b ≤ c)
    (hle : 1 ≤ b) :
    a ≤ c :=
  (le_mul_of_one_le_right' hle).trans h

Left multiplication by element greater than or equal to one preserves order inequality

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b, c \in \alpha$, if $a \cdot b \leq c$ and $1 \leq b$, then $a \leq c$.

lt_of_lt_mul_of_le_one_left theorem

[MulLeftMono α] {a b c : α} (h : a < b * c) (hle : c ≤ 1) : a < b

Full source

@[to_additive]
theorem lt_of_lt_mul_of_le_one_left [MulLeftMono α] {a b c : α} (h : a < b * c)
    (hle : c ≤ 1) :
    a < b :=
  h.trans_le (mul_le_of_le_one_right' hle)

Left multiplication by element less than or equal to one preserves strict order in left-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c \in \alpha$ with $a < b \cdot c$ and $c \leq 1$, we have $a < b$.

le_of_le_mul_of_le_one_left theorem

[MulLeftMono α] {a b c : α} (h : a ≤ b * c) (hle : c ≤ 1) : a ≤ b

Full source

@[to_additive]
theorem le_of_le_mul_of_le_one_left [MulLeftMono α] {a b c : α} (h : a ≤ b * c)
    (hle : c ≤ 1) :
    a ≤ b :=
  h.trans (mul_le_of_le_one_right' hle)

Left multiplication by element less than or equal to one preserves order in left-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b, c \in \alpha$, if $a \leq b \cdot c$ and $c \leq 1$, then $a \leq b$.

lt_of_mul_lt_of_one_le_right theorem

[MulRightMono α] {a b c : α} (h : a * b < c) (hle : 1 ≤ a) : b < c

Full source

@[to_additive]
theorem lt_of_mul_lt_of_one_le_right [MulRightMono α] {a b c : α}
    (h : a * b < c) (hle : 1 ≤ a) :
    b < c :=
  (le_mul_of_one_le_left' hle).trans_lt h

Right multiplication by element greater than or equal to one preserves strict order

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c \in \alpha$ such that $a \cdot b < c$ and $1 \leq a$, we have $b < c$.

le_of_mul_le_of_one_le_right theorem

[MulRightMono α] {a b c : α} (h : a * b ≤ c) (hle : 1 ≤ a) : b ≤ c

Full source

@[to_additive]
theorem le_of_mul_le_of_one_le_right [MulRightMono α] {a b c : α}
    (h : a * b ≤ c) (hle : 1 ≤ a) :
    b ≤ c :=
  (le_mul_of_one_le_left' hle).trans h

Right multiplication by element greater than or equal to one preserves order in right-monotone structures

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a, b, c \in \alpha$ such that $a \cdot b \leq c$ and $1 \leq a$, we have $b \leq c$.

lt_of_lt_mul_of_le_one_right theorem

[MulRightMono α] {a b c : α} (h : a < b * c) (hle : b ≤ 1) : a < c

Full source

@[to_additive]
theorem lt_of_lt_mul_of_le_one_right [MulRightMono α] {a b c : α}
    (h : a < b * c) (hle : b ≤ 1) :
    a < c :=
  h.trans_le (mul_le_of_le_one_left' hle)

Strict inequality preservation under right multiplication by element less than or equal to one

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). For any elements $a, b, c \in \alpha$ with $a < b \cdot c$ and $b \leq 1$, we have $a < c$.

le_of_le_mul_of_le_one_right theorem

[MulRightMono α] {a b c : α} (h : a ≤ b * c) (hle : b ≤ 1) : a ≤ c

Full source

@[to_additive]
theorem le_of_le_mul_of_le_one_right [MulRightMono α] {a b c : α}
    (h : a ≤ b * c) (hle : b ≤ 1) :
    a ≤ c :=
  h.trans (mul_le_of_le_one_left' hle)

Right multiplication by element less than or equal to one preserves order inequality

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b, c \in \alpha$ with $a \leq b \cdot c$ and $b \leq 1$, we have $a \leq c$.

mul_eq_one_iff_of_one_le theorem

[MulLeftMono α] [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : a * b = 1 ↔ a = 1 ∧ b = 1

Full source

@[to_additive]
theorem mul_eq_one_iff_of_one_le [MulLeftMono α]
    [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
    a * b = 1 ↔ a = 1 ∧ b = 1 :=
  Iff.intro
    (fun hab : a * b = 1 =>
      have : a ≤ 1 := hab ▸ le_mul_of_le_of_one_le le_rfl hb
      have : a = 1 := le_antisymm this ha
      have : b ≤ 1 := hab ▸ le_mul_of_one_le_of_le ha le_rfl
      have : b = 1 := le_antisymm this hb
      And.intro ‹a = 1› ‹b = 1›)
    (by rintro ⟨rfl, rfl⟩; rw [mul_one])

Product Equals One iff Both Factors Equal One Under Monotonicity Conditions

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone and right-monotone. For any elements $a, b \in \alpha$ with $1 \leq a$ and $1 \leq b$, the product $a \cdot b$ equals $1$ if and only if both $a = 1$ and $b = 1$.

exists_square_le theorem

[MulLeftStrictMono α] (a : α) : ∃ b : α, b * b ≤ a

Full source

theorem exists_square_le [MulLeftStrictMono α] (a : α) : ∃ b : α, b * b ≤ a := by
  by_cases h : a < 1
  · use a
    have : a * a < a * 1 := mul_lt_mul_left' h a
    rw [mul_one] at this
    exact le_of_lt this
  · use 1
    push_neg at h
    rwa [mul_one]

Existence of Square Root in Left Strictly Monotone Ordered Monoids: $\exists b, b^2 \leq a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation, where left multiplication is strictly monotone (i.e., the function $x \mapsto a * x$ is strictly increasing for any fixed $a$). Then for any element $a \in \alpha$, there exists an element $b \in \alpha$ such that $b \cdot b \leq a$.

Contravariant.toLeftCancelSemigroup definition

[MulLeftReflectLE α] : LeftCancelSemigroup α

Full source

/-- A semigroup with a partial order and satisfying `LeftCancelSemigroup`
(i.e. `a * c < b * c → a < b`) is a `LeftCancelSemigroup`. -/
@[to_additive
"An additive semigroup with a partial order and satisfying `AddLeftCancelSemigroup`
(i.e. `c + a < c + b → a < b`) is a `AddLeftCancelSemigroup`."]
def Contravariant.toLeftCancelSemigroup [MulLeftReflectLE α] :
    LeftCancelSemigroup α :=
  { ‹Semigroup α› with mul_left_cancel := fun _ _ _ => mul_left_cancel'' }

Left Cancellative Semigroup from Order-Reflecting Multiplication

Informal description

Given a semigroup $\alpha$ with a partial order and the property that multiplication on the left reflects the order (i.e., for all $a, b, c \in \alpha$, if $a * b \leq a * c$ then $b \leq c$), then $\alpha$ is a left cancellative semigroup. In other words, the semigroup operation satisfies left cancellation: for all $a, b, c \in \alpha$, if $a * b = a * c$ then $b = c$.

Contravariant.toRightCancelSemigroup definition

[MulRightReflectLE α] : RightCancelSemigroup α

Full source

/-- A semigroup with a partial order and satisfying `RightCancelSemigroup`
(i.e. `a * c < b * c → a < b`) is a `RightCancelSemigroup`. -/
@[to_additive
"An additive semigroup with a partial order and satisfying `AddRightCancelSemigroup`
(`a + c < b + c → a < b`) is a `AddRightCancelSemigroup`."]
def Contravariant.toRightCancelSemigroup [MulRightReflectLE α] :
    RightCancelSemigroup α :=
  { ‹Semigroup α› with mul_right_cancel := fun _ _ _ => mul_right_cancel'' }

Right Cancellative Semigroup from Order-Reflecting Right Multiplication

Informal description

Given a semigroup $\alpha$ with a partial order and the property that multiplication on the right reflects the order (i.e., for all $a, b, c \in \alpha$, if $b * a \leq c * a$ implies $b \leq c$), then $\alpha$ is a right cancellative semigroup. In other words, the semigroup operation satisfies right cancellation: for all $a, b, c \in \alpha$, if $b * a = c * a$ then $b = c$.

Monotone.const_mul' theorem

[MulLeftMono α] (hf : Monotone f) (a : α) : Monotone fun x ↦ a * f x

Full source

@[to_additive const_add]
theorem Monotone.const_mul' [MulLeftMono α] (hf : Monotone f) (a : α) : Monotone fun x ↦ a * f x :=
  mul_left_mono.comp hf

Left Multiplication Preserves Monotonicity: $x \mapsto a \cdot f(x)$ is Monotone When $f$ is Monotone

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a \in \alpha$). If $f : \beta \to \alpha$ is a monotone function between preorders, then for any fixed element $a \in \alpha$, the function $x \mapsto a \cdot f(x)$ is monotone.

MonotoneOn.const_mul' theorem

[MulLeftMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a * f x) s

Full source

@[to_additive const_add]
theorem MonotoneOn.const_mul' [MulLeftMono α] (hf : MonotoneOn f s) (a : α) :
    MonotoneOn (fun x => a * f x) s := mul_left_mono.comp_monotoneOn hf

Left Multiplication Preserves Monotonicity on a Subset: $x \mapsto a \cdot f(x)$ is Monotone on $s$ When $f$ is Monotone on $s$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a \in \alpha$). If $f \colon \beta \to \alpha$ is a function that is monotone on a subset $s \subseteq \beta$, then for any fixed element $a \in \alpha$, the function $x \mapsto a \cdot f(x)$ is monotone on $s$.

Antitone.const_mul' theorem

[MulLeftMono α] (hf : Antitone f) (a : α) : Antitone fun x ↦ a * f x

Full source

@[to_additive const_add]
theorem Antitone.const_mul' [MulLeftMono α] (hf : Antitone f) (a : α) : Antitone fun x ↦ a * f x :=
  mul_left_mono.comp_antitone hf

Left Multiplication Preserves Antitonicity: $x \mapsto a \cdot f(x)$ is Antitone When $f$ is Antitone

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a \in \alpha$). If $f : \beta \to \alpha$ is an antitone function between preorders, then for any fixed element $a \in \alpha$, the function $x \mapsto a \cdot f(x)$ is antitone.

AntitoneOn.const_mul' theorem

[MulLeftMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => a * f x) s

Full source

@[to_additive const_add]
theorem AntitoneOn.const_mul' [MulLeftMono α] (hf : AntitoneOn f s) (a : α) :
    AntitoneOn (fun x => a * f x) s := mul_left_mono.comp_antitoneOn hf

Left Multiplication Preserves Antitonicity on a Subset: $x \mapsto a \cdot f(x)$ is Antitone on $s$ When $f$ is Antitone on $s$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that left multiplication is monotone (i.e., for any fixed $a \in \alpha$, the function $x \mapsto a * x$ is monotone). If $f : \beta \to \alpha$ is an antitone function on a subset $s \subseteq \beta$, then for any fixed element $a \in \alpha$, the function $x \mapsto a * f(x)$ is antitone on $s$.

Monotone.mul_const' theorem

[MulRightMono α] (hf : Monotone f) (a : α) : Monotone fun x => f x * a

Full source

@[to_additive add_const]
theorem Monotone.mul_const' [MulRightMono α] (hf : Monotone f) (a : α) :
    Monotone fun x => f x * a := mul_right_mono.comp hf

Monotonicity of Right Multiplication by a Fixed Element under a Monotone Function

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that right multiplication is monotone (i.e., for any fixed $a \in \alpha$, the function $x \mapsto x * a$ is monotone). If $f : \alpha \to \alpha$ is a monotone function, then for any fixed element $a \in \alpha$, the function $x \mapsto f(x) * a$ is also monotone.

MonotoneOn.mul_const' theorem

[MulRightMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x * a) s

Full source

@[to_additive add_const]
theorem MonotoneOn.mul_const' [MulRightMono α] (hf : MonotoneOn f s) (a : α) :
    MonotoneOn (fun x => f x * a) s := mul_right_mono.comp_monotoneOn hf

Monotonicity of Right Multiplication by a Fixed Element under a Monotone Function on a Subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that right multiplication is monotone (i.e., for any fixed $a \in \alpha$, the function $x \mapsto x * a$ is monotone). If $f \colon \alpha \to \alpha$ is a function that is monotone on a subset $s \subseteq \alpha$, then for any fixed element $a \in \alpha$, the function $x \mapsto f(x) * a$ is also monotone on $s$.

Antitone.mul_const' theorem

[MulRightMono α] (hf : Antitone f) (a : α) : Antitone fun x ↦ f x * a

Full source

@[to_additive add_const]
theorem Antitone.mul_const' [MulRightMono α] (hf : Antitone f) (a : α) : Antitone fun x ↦ f x * a :=
  mul_right_mono.comp_antitone hf

Antitonicity of Right Multiplication by a Fixed Element under an Antitone Function

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that right multiplication is monotone (i.e., for any fixed $a \in \alpha$, the function $x \mapsto x * a$ is monotone). If $f : \alpha \to \alpha$ is an antitone function, then for any $a \in \alpha$, the function $x \mapsto f(x) * a$ is also antitone.

AntitoneOn.mul_const' theorem

[MulRightMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x * a) s

Full source

@[to_additive add_const]
theorem AntitoneOn.mul_const' [MulRightMono α] (hf : AntitoneOn f s) (a : α) :
    AntitoneOn (fun x => f x * a) s := mul_right_mono.comp_antitoneOn hf

Antitonicity of Right Multiplication by a Fixed Element under an Antitone Function on a Subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that right multiplication is monotone (i.e., for any fixed $a \in \alpha$, the function $x \mapsto x * a$ is monotone). If $f : \alpha \to \alpha$ is an antitone function on a subset $s \subseteq \alpha$, then for any $a \in \alpha$, the function $x \mapsto f(x) * a$ is also antitone on $s$.

Monotone.mul' theorem

[MulLeftMono α] [MulRightMono α] (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x * g x

Full source

/-- The product of two monotone functions is monotone. -/
@[to_additive add "The sum of two monotone functions is monotone."]
theorem Monotone.mul' [MulLeftMono α]
    [MulRightMono α] (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x => f x * g x := fun _ _ h => mul_le_mul' (hf h) (hg h)

Monotonicity of Pointwise Product of Monotone Functions

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). If $f, g : \alpha \to \alpha$ are monotone functions, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also monotone.

MonotoneOn.mul' theorem

[MulLeftMono α] [MulRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x * g x) s

Full source

/-- The product of two monotone functions is monotone. -/
@[to_additive add "The sum of two monotone functions is monotone."]
theorem MonotoneOn.mul' [MulLeftMono α]
    [MulRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => f x * g x) s := fun _ hx _ hy h =>
  mul_le_mul' (hf hx hy h) (hg hx hy h)

Monotonicity of Pointwise Product of Monotone Functions on a Subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). If $f, g : \alpha \to \alpha$ are monotone functions on a subset $s \subseteq \alpha$, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also monotone on $s$.

Antitone.mul' theorem

[MulLeftMono α] [MulRightMono α] (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x * g x

Full source

/-- The product of two antitone functions is antitone. -/
@[to_additive add "The sum of two antitone functions is antitone."]
theorem Antitone.mul' [MulLeftMono α]
    [MulRightMono α] (hf : Antitone f) (hg : Antitone g) :
    Antitone fun x => f x * g x := fun _ _ h => mul_le_mul' (hf h) (hg h)

Antitonicity of Pointwise Product of Antitone Functions

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). If $f, g : \alpha \to \alpha$ are antitone functions, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also antitone.

AntitoneOn.mul' theorem

[MulLeftMono α] [MulRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x * g x) s

Full source

/-- The product of two antitone functions is antitone. -/
@[to_additive add "The sum of two antitone functions is antitone."]
theorem AntitoneOn.mul' [MulLeftMono α]
    [MulRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => f x * g x) s :=
  fun _ hx _ hy h => mul_le_mul' (hf hx hy h) (hg hx hy h)

Antitonicity of Pointwise Product of Antitone Functions on a Subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is both left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). If $f, g : \alpha \to \alpha$ are antitone functions on a subset $s \subseteq \alpha$, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also antitone on $s$.

StrictMono.const_mul' theorem

(hf : StrictMono f) (c : α) : StrictMono fun x => c * f x

Full source

@[to_additive const_add]
theorem StrictMono.const_mul' (hf : StrictMono f) (c : α) : StrictMono fun x => c * f x :=
  fun _ _ ab => mul_lt_mul_left' (hf ab) c

Left multiplication preserves strict monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder. If $f : \alpha \to \alpha$ is a strictly monotone function and $c \in \alpha$, then the function $x \mapsto c * f(x)$ is also strictly monotone.

StrictMonoOn.const_mul' theorem

(hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => c * f x) s

Full source

@[to_additive const_add]
theorem StrictMonoOn.const_mul' (hf : StrictMonoOn f s) (c : α) :
    StrictMonoOn (fun x => c * f x) s :=
  fun _ ha _ hb ab => mul_lt_mul_left' (hf ha hb ab) c

Left Multiplication Preserves Strict Monotonicity on a Subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder. If $f : \alpha \to \alpha$ is strictly monotone on a subset $s \subseteq \alpha$, then for any fixed element $c \in \alpha$, the function $x \mapsto c * f(x)$ is strictly monotone on $s$.

StrictAnti.const_mul' theorem

(hf : StrictAnti f) (c : α) : StrictAnti fun x => c * f x

Full source

@[to_additive const_add]
theorem StrictAnti.const_mul' (hf : StrictAnti f) (c : α) : StrictAnti fun x => c * f x :=
  fun _ _ ab => mul_lt_mul_left' (hf ab) c

Left multiplication preserves strict antitonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder. If $f : \alpha \to \alpha$ is a strictly antitone function and $c \in \alpha$ is a fixed element, then the function $x \mapsto c * f(x)$ is also strictly antitone.

StrictAntiOn.const_mul' theorem

(hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => c * f x) s

Full source

@[to_additive const_add]
theorem StrictAntiOn.const_mul' (hf : StrictAntiOn f s) (c : α) :
    StrictAntiOn (fun x => c * f x) s :=
  fun _ ha _ hb ab => mul_lt_mul_left' (hf ha hb ab) c

Left multiplication preserves strict antitonicity on a subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder, and let $f : \alpha \to \alpha$ be a function that is strictly antitone on a subset $s \subseteq \alpha$. Then for any fixed element $c \in \alpha$, the function $x \mapsto c * f(x)$ is strictly antitone on $s$.

StrictMono.mul_const' theorem

(hf : StrictMono f) (c : α) : StrictMono fun x => f x * c

Full source

@[to_additive add_const]
theorem StrictMono.mul_const' (hf : StrictMono f) (c : α) : StrictMono fun x => f x * c :=
  fun _ _ ab => mul_lt_mul_right' (hf ab) c

Right multiplication preserves strict monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If $f : \alpha \to \alpha$ is a strictly monotone function and $c \in \alpha$ is a fixed element, then the function $x \mapsto f(x) * c$ is also strictly monotone.

StrictMonoOn.mul_const' theorem

(hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x * c) s

Full source

@[to_additive add_const]
theorem StrictMonoOn.mul_const' (hf : StrictMonoOn f s) (c : α) :
    StrictMonoOn (fun x => f x * c) s :=
  fun _ ha _ hb ab => mul_lt_mul_right' (hf ha hb ab) c

Right multiplication preserves strict monotonicity on a subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder, and let $f : \alpha \to \alpha$ be a function that is strictly monotone on a subset $s \subseteq \alpha$. Then for any fixed element $c \in \alpha$, the function $x \mapsto f(x) * c$ is strictly monotone on $s$.

StrictAnti.mul_const' theorem

(hf : StrictAnti f) (c : α) : StrictAnti fun x => f x * c

Full source

@[to_additive add_const]
theorem StrictAnti.mul_const' (hf : StrictAnti f) (c : α) : StrictAnti fun x => f x * c :=
  fun _ _ ab => mul_lt_mul_right' (hf ab) c

Right multiplication preserves strict antitonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If $f : \alpha \to \alpha$ is a strictly antitone function and $c \in \alpha$ is a fixed element, then the function $x \mapsto f(x) * c$ is also strictly antitone.

StrictAntiOn.mul_const' theorem

(hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => f x * c) s

Full source

@[to_additive add_const]
theorem StrictAntiOn.mul_const' (hf : StrictAntiOn f s) (c : α) :
    StrictAntiOn (fun x => f x * c) s :=
  fun _ ha _ hb ab => mul_lt_mul_right' (hf ha hb ab) c

Right multiplication preserves strict antitonicity on a subset

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order relation. If $f : \alpha \to \alpha$ is strictly antitone on a subset $s \subseteq \alpha$ and $c \in \alpha$ is a fixed element, then the function $x \mapsto f(x) * c$ is strictly antitone on $s$.

StrictMono.mul' theorem

[MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) : StrictMono fun x => f x * g x

Full source

/-- The product of two strictly monotone functions is strictly monotone. -/
@[to_additive add "The sum of two strictly monotone functions is strictly monotone."]
theorem StrictMono.mul' [MulLeftStrictMono α]
    [MulRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) :
    StrictMono fun x => f x * g x := fun _ _ ab =>
  mul_lt_mul_of_lt_of_lt (hf ab) (hg ab)

Product of Strictly Monotone Functions is Strictly Monotone

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order such that multiplication is both left-strictly-monotone (i.e., $x \mapsto a \cdot x$ is strictly increasing for any fixed $a$) and right-strictly-monotone (i.e., $x \mapsto x \cdot a$ is strictly increasing for any fixed $a$). If $f, g : \alpha \to \alpha$ are strictly monotone functions, then their pointwise product $x \mapsto f(x) \cdot g(x)$ is also strictly monotone.

StrictMonoOn.mul' theorem

 [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn g s) :
  StrictMonoOn (fun x => f x * g x) s

Full source

/-- The product of two strictly monotone functions is strictly monotone. -/
@[to_additive add "The sum of two strictly monotone functions is strictly monotone."]
theorem StrictMonoOn.mul' [MulLeftStrictMono α]
    [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn g s) :
    StrictMonoOn (fun x => f x * g x) s :=
  fun _ ha _ hb ab => mul_lt_mul_of_lt_of_lt (hf ha hb ab) (hg ha hb ab)

Product of Strictly Monotone Functions on a Subset is Strictly Monotone

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order such that multiplication is both left-strictly-monotone (i.e., $x \mapsto a \cdot x$ is strictly increasing for any fixed $a$) and right-strictly-monotone (i.e., $x \mapsto x \cdot a$ is strictly increasing for any fixed $a$). Given two functions $f, g : \alpha \to \alpha$ that are strictly monotone on a subset $s \subseteq \alpha$, their pointwise product $x \mapsto f(x) \cdot g(x)$ is strictly monotone on $s$.

StrictAnti.mul' theorem

[MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti fun x => f x * g x

Full source

/-- The product of two strictly antitone functions is strictly antitone. -/
@[to_additive add "The sum of two strictly antitone functions is strictly antitone."]
theorem StrictAnti.mul' [MulLeftStrictMono α]
    [MulRightStrictMono α] (hf : StrictAnti f) (hg : StrictAnti g) :
    StrictAnti fun x => f x * g x :=
  fun _ _ ab => mul_lt_mul_of_lt_of_lt (hf ab) (hg ab)

Product of Strictly Antitone Functions is Strictly Antitone

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order such that multiplication is both left-strictly-monotone (i.e., $x \mapsto a \cdot x$ is strictly increasing for any fixed $a$) and right-strictly-monotone (i.e., $x \mapsto x \cdot a$ is strictly increasing for any fixed $a$). If $f, g : \alpha \to \alpha$ are strictly antitone functions, then their pointwise product $x \mapsto f(x) \cdot g(x)$ is also strictly antitone.

StrictAntiOn.mul' theorem

 [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) :
  StrictAntiOn (fun x => f x * g x) s

Full source

/-- The product of two strictly antitone functions is strictly antitone. -/
@[to_additive add "The sum of two strictly antitone functions is strictly antitone."]
theorem StrictAntiOn.mul' [MulLeftStrictMono α]
    [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) :
    StrictAntiOn (fun x => f x * g x) s :=
  fun _ ha _ hb ab => mul_lt_mul_of_lt_of_lt (hf ha hb ab) (hg ha hb ab)

Product of Strictly Antitone Functions on a Subset is Strictly Antitone

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder such that multiplication is both left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). Given two functions $f, g : \alpha \to \alpha$ that are strictly antitone on a subset $s \subseteq \alpha$, the product function $x \mapsto f(x) \cdot g(x)$ is strictly antitone on $s$.

Monotone.mul_strictMono' theorem

 [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : Monotone f) (hg : StrictMono g) :
  StrictMono fun x => f x * g x

Full source

/-- The product of a monotone function and a strictly monotone function is strictly monotone. -/
@[to_additive add_strictMono "The sum of a monotone function and a strictly monotone function is
strictly monotone."]
theorem Monotone.mul_strictMono' [MulLeftStrictMono α]
    [MulRightMono α] {f g : β → α} (hf : Monotone f)
    (hg : StrictMono g) :
    StrictMono fun x => f x * g x :=
  fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)

Product of Monotone and Strictly Monotone Functions is Strictly Monotone

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Given two functions $f, g : \beta \to \alpha$ where $f$ is monotone and $g$ is strictly monotone, the product function $x \mapsto f(x) \cdot g(x)$ is strictly monotone.

MonotoneOn.mul_strictMono' theorem

 [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) :
  StrictMonoOn (fun x => f x * g x) s

Full source

/-- The product of a monotone function and a strictly monotone function is strictly monotone. -/
@[to_additive add_strictMono "The sum of a monotone function and a strictly monotone function is
strictly monotone."]
theorem MonotoneOn.mul_strictMono' [MulLeftStrictMono α]
    [MulRightMono α] {f g : β → α} (hf : MonotoneOn f s)
    (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x * g x) s :=
  fun _ hx _ hy h => mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)

Product of Monotone and Strictly Monotone Functions on a Subset is Strictly Monotone

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Given two functions $f, g : \beta \to \alpha$ where $f$ is monotone on a subset $s \subseteq \beta$ and $g$ is strictly monotone on $s$, the product function $x \mapsto f(x) \cdot g(x)$ is strictly monotone on $s$.

Antitone.mul_strictAnti' theorem

 [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : Antitone f) (hg : StrictAnti g) :
  StrictAnti fun x => f x * g x

Full source

/-- The product of an antitone function and a strictly antitone function is strictly antitone. -/
@[to_additive add_strictAnti "The sum of an antitone function and a strictly antitone function is
strictly antitone."]
theorem Antitone.mul_strictAnti' [MulLeftStrictMono α]
    [MulRightMono α] {f g : β → α} (hf : Antitone f)
    (hg : StrictAnti g) :
    StrictAnti fun x => f x * g x :=
  fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)

Product of Antitone and Strictly Antitone Functions is Strictly Antitone

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Given two functions $f, g : \beta \to \alpha$ where $f$ is antitone and $g$ is strictly antitone, the product function $x \mapsto f(x) \cdot g(x)$ is strictly antitone.

AntitoneOn.mul_strictAnti' theorem

 [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) :
  StrictAntiOn (fun x => f x * g x) s

Full source

/-- The product of an antitone function and a strictly antitone function is strictly antitone. -/
@[to_additive add_strictAnti "The sum of an antitone function and a strictly antitone function is
strictly antitone."]
theorem AntitoneOn.mul_strictAnti' [MulLeftStrictMono α]
    [MulRightMono α] {f g : β → α} (hf : AntitoneOn f s)
    (hg : StrictAntiOn g s) :
    StrictAntiOn (fun x => f x * g x) s :=
  fun _ hx _ hy h => mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)

Product of Antitone and Strictly Antitone Functions on a Subset is Strictly Antitone

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Given two functions $f, g : \beta \to \alpha$ where $f$ is antitone on a subset $s \subseteq \beta$ and $g$ is strictly antitone on $s$, the product function $x \mapsto f(x) \cdot g(x)$ is strictly antitone on $s$.

StrictMono.mul_monotone' theorem

(hf : StrictMono f) (hg : Monotone g) : StrictMono fun x => f x * g x

Full source

/-- The product of a strictly monotone function and a monotone function is strictly monotone. -/
@[to_additive add_monotone "The sum of a strictly monotone function and a monotone function is
strictly monotone."]
theorem StrictMono.mul_monotone' (hf : StrictMono f) (hg : Monotone g) :
    StrictMono fun x => f x * g x :=
  fun _ _ h => mul_lt_mul_of_lt_of_le (hf h) (hg h.le)

Product of Strictly Monotone and Monotone Functions is Strictly Monotone

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function and $g : \alpha \to \beta$ be a monotone function between preorders. Then the product function $x \mapsto f(x) \cdot g(x)$ is strictly monotone.

StrictMonoOn.mul_monotone' theorem

(hf : StrictMonoOn f s) (hg : MonotoneOn g s) : StrictMonoOn (fun x => f x * g x) s

Full source

/-- The product of a strictly monotone function and a monotone function is strictly monotone. -/
@[to_additive add_monotone "The sum of a strictly monotone function and a monotone function is
strictly monotone."]
theorem StrictMonoOn.mul_monotone' (hf : StrictMonoOn f s) (hg : MonotoneOn g s) :
    StrictMonoOn (fun x => f x * g x) s :=
  fun _ hx _ hy h => mul_lt_mul_of_lt_of_le (hf hx hy h) (hg hx hy h.le)

Product of Strictly Monotone and Monotone Functions on a Subset is Strictly Monotone

Informal description

Let $f, g : \alpha \to \beta$ be functions between preorders, and let $s \subseteq \alpha$. If $f$ is strictly monotone on $s$ and $g$ is monotone on $s$, then the product function $x \mapsto f(x) \cdot g(x)$ is strictly monotone on $s$.

StrictAnti.mul_antitone' theorem

(hf : StrictAnti f) (hg : Antitone g) : StrictAnti fun x => f x * g x

Full source

/-- The product of a strictly antitone function and an antitone function is strictly antitone. -/
@[to_additive add_antitone "The sum of a strictly antitone function and an antitone function is
strictly antitone."]
theorem StrictAnti.mul_antitone' (hf : StrictAnti f) (hg : Antitone g) :
    StrictAnti fun x => f x * g x :=
  fun _ _ h => mul_lt_mul_of_lt_of_le (hf h) (hg h.le)

Strictly Antitone Function Multiplied by Antitone Function is Strictly Antitone

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function and $g : \alpha \to \beta$ be an antitone function between preorders. Then the product function $x \mapsto f(x) \cdot g(x)$ is strictly antitone.

StrictAntiOn.mul_antitone' theorem

(hf : StrictAntiOn f s) (hg : AntitoneOn g s) : StrictAntiOn (fun x => f x * g x) s

Full source

/-- The product of a strictly antitone function and an antitone function is strictly antitone. -/
@[to_additive add_antitone "The sum of a strictly antitone function and an antitone function is
strictly antitone."]
theorem StrictAntiOn.mul_antitone' (hf : StrictAntiOn f s) (hg : AntitoneOn g s) :
    StrictAntiOn (fun x => f x * g x) s :=
  fun _ hx _ hy h => mul_lt_mul_of_lt_of_le (hf hx hy h) (hg hx hy h.le)

Product of Strictly Antitone and Antitone Functions on a Subset is Strictly Antitone

Informal description

Let $f, g : \alpha \to \beta$ be functions between preorders, and let $s \subseteq \alpha$. If $f$ is strictly antitone on $s$ and $g$ is antitone on $s$, then the product function $x \mapsto f(x) \cdot g(x)$ is strictly antitone on $s$.

cmp_mul_left' theorem

{α : Type*} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (a b c : α) : cmp (a * b) (a * c) = cmp b c

Full source

@[to_additive (attr := simp) cmp_add_left]
theorem cmp_mul_left' {α : Type*} [Mul α] [LinearOrder α] [MulLeftStrictMono α]
    (a b c : α) :
    cmp (a * b) (a * c) = cmp b c :=
  (strictMono_id.const_mul' a).cmp_map_eq b c

Left Multiplication Preserves Comparison: $\mathrm{cmp}(a \cdot b, a \cdot c) = \mathrm{cmp}(b, c)$

Informal description

Let $\alpha$ be a linearly ordered type with a multiplication operation that is strictly monotone in its left argument. For any elements $a, b, c \in \alpha$, the comparison of $a \cdot b$ and $a \cdot c$ is equal to the comparison of $b$ and $c$, i.e., $\mathrm{cmp}(a \cdot b, a \cdot c) = \mathrm{cmp}(b, c)$.

cmp_mul_right' theorem

{α : Type*} [Mul α] [LinearOrder α] [MulRightStrictMono α] (a b c : α) : cmp (a * c) (b * c) = cmp a b

Full source

@[to_additive (attr := simp) cmp_add_right]
theorem cmp_mul_right' {α : Type*} [Mul α] [LinearOrder α]
    [MulRightStrictMono α] (a b c : α) :
    cmp (a * c) (b * c) = cmp a b :=
  (strictMono_id.mul_const' c).cmp_map_eq a b

Right Multiplication Preserves Comparison: $\mathrm{cmp}(a \cdot c, b \cdot c) = \mathrm{cmp}(a, b)$

Informal description

Let $\alpha$ be a linearly ordered type with a multiplication operation that is strictly monotone in the right argument. Then for any elements $a, b, c \in \alpha$, the comparison of $a \cdot c$ and $b \cdot c$ is equal to the comparison of $a$ and $b$, i.e., $\mathrm{cmp}(a \cdot c, b \cdot c) = \mathrm{cmp}(a, b)$.

MulLECancellable definition

[Mul α] [LE α] (a : α) : Prop

Full source

/-- An element `a : α` is `MulLECancellable` if `x ↦ a * x` is order-reflecting.
We will make a separate version of many lemmas that require `[MulLeftReflectLE α]` with
`MulLECancellable` assumptions instead. These lemmas can then be instantiated to specific types,
like `ENNReal`, where we can replace the assumption `AddLECancellable x` by `x ≠ ∞`.
-/
@[to_additive
"An element `a : α` is `AddLECancellable` if `x ↦ a + x` is order-reflecting.
We will make a separate version of many lemmas that require `[MulLeftReflectLE α]` with
`AddLECancellable` assumptions instead. These lemmas can then be instantiated to specific types,
like `ENNReal`, where we can replace the assumption `AddLECancellable x` by `x ≠ ∞`. "]
def MulLECancellable [Mul α] [LE α] (a : α) : Prop :=
  ∀ ⦃b c⦄, a * b ≤ a * c → b ≤ c

Multiplicative left order-cancellable element

Informal description

An element $a$ in a multiplicative type $\alpha$ with a preorder is called *multiplicative left order-cancellable* if for any elements $b, c \in \alpha$, the inequality $a \cdot b \leq a \cdot c$ implies $b \leq c$. In other words, left multiplication by $a$ reflects the order relation.

Contravariant.MulLECancellable theorem

[Mul α] [LE α] [MulLeftReflectLE α] {a : α} : MulLECancellable a

Full source

@[to_additive]
theorem Contravariant.MulLECancellable [Mul α] [LE α] [MulLeftReflectLE α]
    {a : α} :
    MulLECancellable a :=
  fun _ _ => le_of_mul_le_mul_left'

Every element is left order-cancellable under left-reflecting multiplication

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, such that multiplication on the left reflects the order (i.e., satisfies the condition `MulLeftReflectLE`). Then every element $a \in \alpha$ is multiplicative left order-cancellable, meaning that for any $b, c \in \alpha$, the inequality $a \cdot b \leq a \cdot c$ implies $b \leq c$.

mulLECancellable_one theorem

[MulOneClass α] [LE α] : MulLECancellable (1 : α)

Full source

@[to_additive (attr := simp)]
theorem mulLECancellable_one [MulOneClass α] [LE α] : MulLECancellable (1 : α) := fun a b => by
  simpa only [one_mul] using id

Identity Element is Left Order-Cancellable in MulOneClass

Informal description

In a multiplicative structure $\alpha$ with a multiplicative identity $1$ and a preorder relation $\leq$, the identity element $1$ is multiplicative left order-cancellable. That is, for any elements $b, c \in \alpha$, the inequality $1 \cdot b \leq 1 \cdot c$ implies $b \leq c$.

MulLECancellable.Injective theorem

[Mul α] [PartialOrder α] {a : α} (ha : MulLECancellable a) : Injective (a * ·)

Full source

@[to_additive]
protected theorem Injective [Mul α] [PartialOrder α] {a : α} (ha : MulLECancellable a) :
    Injective (a * ·) :=
  fun _ _ h => le_antisymm (ha h.le) (ha h.ge)

Injectivity of Left Multiplication by an Order-Cancellable Element

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order. For any element $a \in \alpha$ that is multiplicative left order-cancellable, the left multiplication map $x \mapsto a * x$ is injective. In other words, if $a * b = a * c$ for some $b, c \in \alpha$, then $b = c$.

MulLECancellable.inj theorem

[Mul α] [PartialOrder α] {a b c : α} (ha : MulLECancellable a) : a * b = a * c ↔ b = c

Full source

@[to_additive]
protected theorem inj [Mul α] [PartialOrder α] {a b c : α} (ha : MulLECancellable a) :
    a * b = a * c ↔ b = c :=
  ha.Injective.eq_iff

Equivalence of Left Multiplication by an Order-Cancellable Element

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order. For any multiplicative left order-cancellable element $a \in \alpha$ and any elements $b, c \in \alpha$, the equality $a * b = a * c$ holds if and only if $b = c$.

MulLECancellable.injective_left theorem

[Mul α] [i : @Std.Commutative α (· * ·)] [PartialOrder α] {a : α} (ha : MulLECancellable a) : Injective (· * a)

Full source

@[to_additive]
protected theorem injective_left [Mul α] [i : @Std.Commutative α (· * ·)] [PartialOrder α] {a : α}
    (ha : MulLECancellable a) :
    Injective (· * a) := fun b c h => ha.Injective <| by dsimp; rwa [i.comm a, i.comm a]

Injectivity of Right Multiplication by an Order-Cancellable Element in a Commutative Setting

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order, where multiplication is commutative. For any element $a \in \alpha$ that is multiplicative left order-cancellable, the right multiplication map $x \mapsto x * a$ is injective. In other words, if $b * a = c * a$ for some $b, c \in \alpha$, then $b = c$.

MulLECancellable.inj_left theorem

 [Mul α] [@Std.Commutative α (· * ·)] [PartialOrder α] {a b c : α} (hc : MulLECancellable c) : a * c = b * c ↔ a = b

Full source

@[to_additive]
protected theorem inj_left [Mul α] [@Std.Commutative α (· * ·)] [PartialOrder α] {a b c : α}
    (hc : MulLECancellable c) :
    a * c = b * c ↔ a = b :=
  hc.injective_left.eq_iff

Right Cancellation Property for Order-Cancellable Elements in Commutative Monoids

Informal description

Let $\alpha$ be a type with a commutative multiplication operation and a partial order. For any elements $a, b, c \in \alpha$ where $c$ is multiplicative left order-cancellable, the equality $a \cdot c = b \cdot c$ holds if and only if $a = b$.

MulLECancellable.mul_le_mul_iff_left theorem

[Mul α] [MulLeftMono α] {a b c : α} (ha : MulLECancellable a) : a * b ≤ a * c ↔ b ≤ c

Full source

@[to_additive]
protected theorem mul_le_mul_iff_left [Mul α] [MulLeftMono α] {a b c : α}
    (ha : MulLECancellable a) : a * b ≤ a * c ↔ b ≤ c :=
  ⟨fun h => ha h, fun h => mul_le_mul_left' h a⟩

Left Multiplication Preserves Order Iff for Cancellable Elements

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b, c \in \alpha$ where $a$ is multiplicative left order-cancellable, we have the equivalence $a \cdot b \leq a \cdot c$ if and only if $b \leq c$.

MulLECancellable.mul_le_mul_iff_right theorem

 [Mul α] [i : @Std.Commutative α (· * ·)] [MulLeftMono α] {a b c : α} (ha : MulLECancellable a) : b * a ≤ c * a ↔ b ≤ c

Full source

@[to_additive]
protected theorem mul_le_mul_iff_right [Mul α] [i : @Std.Commutative α (· * ·)]
    [MulLeftMono α] {a b c : α} (ha : MulLECancellable a) :
    b * a ≤ c * a ↔ b ≤ c := by rw [i.comm b, i.comm c, ha.mul_le_mul_iff_left]

Right Multiplication Preserves Order Iff for Cancellable Elements in Commutative Monoids

Informal description

Let $\alpha$ be a type with a commutative multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b, c \in \alpha$ where $a$ is multiplicative left order-cancellable, we have the equivalence $b \cdot a \leq c \cdot a$ if and only if $b \leq c$.

MulLECancellable.le_mul_iff_one_le_right theorem

[MulOneClass α] [MulLeftMono α] {a b : α} (ha : MulLECancellable a) : a ≤ a * b ↔ 1 ≤ b

Full source

@[to_additive]
protected theorem le_mul_iff_one_le_right [MulOneClass α] [MulLeftMono α]
    {a b : α} (ha : MulLECancellable a) :
    a ≤ a * b ↔ 1 ≤ b :=
  Iff.trans (by rw [mul_one]) ha.mul_le_mul_iff_left

Order-reflecting property of left multiplication: $a \leq a \cdot b \leftrightarrow 1 \leq b$

Informal description

Let $\alpha$ be a multiplicative monoid with identity element $1$ and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b \in \alpha$ where $a$ is multiplicative left order-cancellable, the inequality $a \leq a \cdot b$ holds if and only if $1 \leq b$.

MulLECancellable.mul_le_iff_le_one_right theorem

[MulOneClass α] [MulLeftMono α] {a b : α} (ha : MulLECancellable a) : a * b ≤ a ↔ b ≤ 1

Full source

@[to_additive]
protected theorem mul_le_iff_le_one_right [MulOneClass α] [MulLeftMono α]
    {a b : α} (ha : MulLECancellable a) :
    a * b ≤ a ↔ b ≤ 1 :=
  Iff.trans (by rw [mul_one]) ha.mul_le_mul_iff_left

Right Multiplication by Cancellable Element Reflects Order with Identity

Informal description

Let $\alpha$ be a multiplicative monoid with identity element $1$ and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b \in \alpha$ where $a$ is multiplicative left order-cancellable, the inequality $a \cdot b \leq a$ holds if and only if $b \leq 1$.

MulLECancellable.le_mul_iff_one_le_left theorem

 [MulOneClass α] [i : @Std.Commutative α (· * ·)] [MulLeftMono α] {a b : α} (ha : MulLECancellable a) :
  a ≤ b * a ↔ 1 ≤ b

Full source

@[to_additive]
protected theorem le_mul_iff_one_le_left [MulOneClass α] [i : @Std.Commutative α (· * ·)]
    [MulLeftMono α] {a b : α} (ha : MulLECancellable a) :
    a ≤ b * a ↔ 1 ≤ b := by rw [i.comm, ha.le_mul_iff_one_le_right]

Order-reflecting property of left multiplication (commutative case): $a \leq b \cdot a \leftrightarrow 1 \leq b$

Informal description

Let $\alpha$ be a multiplicative monoid with identity element $1$ and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Suppose also that multiplication is commutative. For any elements $a, b \in \alpha$ where $a$ is multiplicative left order-cancellable, the inequality $a \leq b \cdot a$ holds if and only if $1 \leq b$.

MulLECancellable.mul_le_iff_le_one_left theorem

 [MulOneClass α] [i : @Std.Commutative α (· * ·)] [MulLeftMono α] {a b : α} (ha : MulLECancellable a) :
  b * a ≤ a ↔ b ≤ 1

Full source

@[to_additive]
protected theorem mul_le_iff_le_one_left [MulOneClass α] [i : @Std.Commutative α (· * ·)]
    [MulLeftMono α] {a b : α} (ha : MulLECancellable a) :
    b * a ≤ a ↔ b ≤ 1 := by rw [i.comm, ha.mul_le_iff_le_one_right]

Commutative Left Order-Cancellable Element Reflects Order via Right Multiplication

Informal description

Let $\alpha$ be a multiplicative monoid with identity element $1$ and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Assume further that multiplication is commutative. For any elements $a, b \in \alpha$ where $a$ is multiplicative left order-cancellable, the inequality $b \cdot a \leq a$ holds if and only if $b \leq 1$.

MulLECancellable.mul theorem

[Semigroup α] {a b : α} (ha : MulLECancellable a) (hb : MulLECancellable b) : MulLECancellable (a * b)

Full source

@[to_additive] lemma mul [Semigroup α] {a b : α} (ha : MulLECancellable a)
    (hb : MulLECancellable b) : MulLECancellable (a * b) :=
  fun c d hcd ↦ hb <| ha <| by rwa [← mul_assoc, ← mul_assoc]

Product of Left Order-Cancellable Elements is Left Order-Cancellable

Informal description

Let $\alpha$ be a semigroup, and let $a, b \in \alpha$ be multiplicative left order-cancellable elements. Then their product $a \cdot b$ is also multiplicative left order-cancellable.

MulLECancellable.of_mul_right theorem

[Semigroup α] [MulLeftMono α] {a b : α} (h : MulLECancellable (a * b)) : MulLECancellable b

Full source

@[to_additive] lemma of_mul_right [Semigroup α] [MulLeftMono α] {a b : α}
    (h : MulLECancellable (a * b)) : MulLECancellable b :=
  fun c d hcd ↦ h <| by rw [mul_assoc, mul_assoc]; exact mul_le_mul_left' hcd _

Right Factor Inherits Left Order-Cancellability in Semigroups

Informal description

Let $\alpha$ be a semigroup with a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). If the product $a \cdot b$ is multiplicative left order-cancellable (i.e., $a \cdot b \cdot x \leq a \cdot b \cdot y$ implies $x \leq y$ for any $x, y$), then $b$ is also multiplicative left order-cancellable.

MulLECancellable.of_mul_left theorem

[CommSemigroup α] [MulLeftMono α] {a b : α} (h : MulLECancellable (a * b)) : MulLECancellable a

Full source

@[to_additive] lemma of_mul_left [CommSemigroup α] [MulLeftMono α] {a b : α}
    (h : MulLECancellable (a * b)) : MulLECancellable a := (mul_comm a b ▸ h).of_mul_right

Left Factor Inherits Left Order-Cancellability in Commutative Semigroups

Informal description

Let $\alpha$ be a commutative semigroup with a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). If the product $a \cdot b$ is multiplicative left order-cancellable (i.e., $a \cdot b \cdot x \leq a \cdot b \cdot y$ implies $x \leq y$ for any $x, y$), then $a$ is also multiplicative left order-cancellable.

mulLECancellable_mul theorem

 [LE α] [CommSemigroup α] [MulLeftMono α] {a b : α} : MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b

Full source

@[to_additive (attr := simp)]
lemma mulLECancellable_mul [LE α] [CommSemigroup α] [MulLeftMono α] {a b : α} :
    MulLECancellableMulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b :=
  ⟨fun h ↦ ⟨h.of_mul_left, h.of_mul_right⟩, fun h ↦ h.1.mul h.2⟩

Product is Left Order-Cancellable if and only if Both Factors Are

Informal description

Let $\alpha$ be a commutative semigroup with a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). For any elements $a, b \in \alpha$, the product $a \cdot b$ is multiplicative left order-cancellable if and only if both $a$ and $b$ are multiplicative left order-cancellable.

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Implementation details

Remark