Lemmas on the monotone multiplication typeclasses

This file builds on Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean by proving several lemmas that do not immediately follow from the typeclass specifications.

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

Assumes left covariance.

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

Alias of Left.mul_pos.

---

Assumes left covariance.

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

@[simp]

theorem mul_pos_iff_of_pos_left {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) : 0 < a * b ↔ 0 < b

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

Assumes right covariance.

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

@[simp]

theorem mul_pos_iff_of_pos_right {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) : 0 < a * b ↔ 0 < a

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

Assumes left covariance.

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

Alias of Left.mul_nonneg.

---

Assumes left covariance.

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

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

Assumes right covariance.

theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

theorem pos_of_mul_pos_right {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulReflectLT α] (h : 0 < a * b) (ha : 0 ≤ a) : 0 < b

theorem pos_of_mul_pos_left {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosReflectLT α] (h : 0 < a * b) (hb : 0 ≤ b) : 0 < a

theorem pos_iff_pos_of_mul_pos {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) : 0 < a ↔ 0 < b

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

Assumes left strict covariance.

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

Assumes right strict covariance.

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

Alias of Left.mul_lt_mul_of_nonneg.

---

Assumes left strict covariance.

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

Alias of Left.mul_lt_mul_of_nonneg.

---

Assumes left strict covariance.

theorem mul_self_le_mul_self {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulMono α] [MulPosMono α] (ha : 0 ≤ a) (hab : a ≤ b) : a * a ≤ b * b

theorem posMulMono_iff_covariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : PosMulMono α ↔ CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2

theorem mulPosMono_iff_covariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : MulPosMono α ↔ CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2

theorem posMulReflectLT_iff_contravariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : PosMulReflectLT α ↔ ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2

theorem mulPosReflectLT_iff_contravariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : MulPosReflectLT α ↔ ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2

@[instance 100]

instance PosMulStrictMono.toPosMulMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] : PosMulMono α

@[instance 100]

instance MulPosStrictMono.toMulPosMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [MulPosStrictMono α] : MulPosMono α

@[instance 100]

instance PosMulReflectLE.toPosMulReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [PosMulReflectLE α] : PosMulReflectLT α

@[instance 100]

instance MulPosReflectLE.toMulPosReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [MulPosReflectLE α] : MulPosReflectLT α

theorem mul_left_cancel_iff_of_pos {α : Type u_1} [MulZeroClass α] {a b c : α} [PartialOrder α] [PosMulReflectLE α] (a0 : 0 < a) : a * b = a * c ↔ b = c

theorem mul_right_cancel_iff_of_pos {α : Type u_1} [MulZeroClass α] {a b c : α} [PartialOrder α] [MulPosReflectLE α] (b0 : 0 < b) : a * b = c * b ↔ a = c

theorem mul_eq_mul_iff_eq_and_eq_of_pos {α : Type u_1} [MulZeroClass α] {a b c d : α} [PartialOrder α] [PosMulStrictMono α] [MulPosStrictMono α] (hab : a ≤ b) (hcd : c ≤ d) (a0 : 0 < a) (d0 : 0 < d) : a * c = b * d ↔ a = b ∧ c = d

theorem mul_eq_mul_iff_eq_and_eq_of_pos' {α : Type u_1} [MulZeroClass α] {a b c d : α} [PartialOrder α] [PosMulStrictMono α] [MulPosStrictMono α] (hab : a ≤ b) (hcd : c ≤ d) (b0 : 0 < b) (c0 : 0 < c) : a * c = b * d ↔ a = b ∧ c = d

theorem eq_and_eq_of_pos_of_le_of_mul_le_mul {α : Type u_1} [MulZeroClass α] {a b c d : α} [PartialOrder α] [PosMulReflectLE α] [MulPosReflectLE α] [PosMulMono α] [MulPosMono α] (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (h : b * d ≤ a * c) : a = b ∧ c = d

theorem PosMulMono.toPosMulStrictMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsLeftCancelMulZero α] [PosMulMono α] : PosMulStrictMono α

theorem posMulMono_iff_posMulStrictMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsLeftCancelMulZero α] : PosMulMono α ↔ PosMulStrictMono α

theorem MulPosMono.toMulPosStrictMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsRightCancelMulZero α] [MulPosMono α] : MulPosStrictMono α

theorem mulPosMono_iff_mulPosStrictMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsRightCancelMulZero α] : MulPosMono α ↔ MulPosStrictMono α

theorem PosMulReflectLT.toPosMulReflectLE {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsLeftCancelMulZero α] [PosMulReflectLT α] : PosMulReflectLE α

theorem posMulReflectLE_iff_posMulReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsLeftCancelMulZero α] : PosMulReflectLE α ↔ PosMulReflectLT α

theorem MulPosReflectLT.toMulPosReflectLE {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsRightCancelMulZero α] [MulPosReflectLT α] : MulPosReflectLE α

theorem mulPosReflectLE_iff_mulPosReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [IsRightCancelMulZero α] : MulPosReflectLE α ↔ MulPosReflectLT α

theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem neg_of_mul_pos_right {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a ≤ 0) : b < 0

theorem neg_of_mul_pos_left {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b ≤ 0) : a < 0

theorem neg_iff_neg_of_mul_pos {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : a < 0 ↔ b < 0

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

theorem neg_of_mul_neg_right {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0

Alias of Left.neg_of_mul_neg_right.

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

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

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

Alias of Left.neg_of_mul_neg_left.

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

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

theorem one_lt_of_lt_mul_left₀ {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulReflectLT α] (ha : 0 ≤ a) (h : a < a * b) : 1 < b

theorem one_lt_of_lt_mul_right₀ {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosReflectLT α] (hb : 0 ≤ b) (h : b < a * b) : 1 < a

theorem one_le_of_le_mul_left₀ {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulReflectLE α] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b

theorem one_le_of_le_mul_right₀ {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosReflectLE α] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a

@[simp]

theorem le_mul_iff_one_le_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a ≤ a * b ↔ 1 ≤ b

@[simp]

theorem lt_mul_iff_one_lt_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a < a * b ↔ 1 < b

@[simp]

theorem mul_le_iff_le_one_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a ↔ b ≤ 1

@[simp]

theorem mul_lt_iff_lt_one_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a * b < a ↔ b < 1

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

@[simp]

theorem le_mul_iff_one_le_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : a ≤ b * a ↔ 1 ≤ b

@[simp]

theorem lt_mul_iff_one_lt_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) : a < b * a ↔ 1 < b

@[simp]

theorem mul_le_iff_le_one_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosMono α] [MulPosReflectLE α] (b0 : 0 < b) : a * b ≤ b ↔ a ≤ 1

@[simp]

theorem mul_lt_iff_lt_one_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (b0 : 0 < b) : a * b < b ↔ a < 1

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

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

theorem mul_le_of_le_one_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b

theorem le_mul_of_one_le_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosMono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b

theorem mul_le_of_le_one_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a

theorem le_mul_of_one_le_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b

theorem mul_lt_of_lt_one_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) : a * b < b

theorem lt_mul_of_one_lt_left {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) : b < a * b

theorem mul_lt_of_lt_one_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) : a * b < a

theorem lt_mul_of_one_lt_right {α : Type u_1} [MulOneClass α] [Zero α] {a b : α} [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (h : 1 < b) : a < a * b

theorem Monotone.mul {α : Type u_1} {M₀ : Type u_2} [Mul M₀] [Zero M₀] [Preorder M₀] [Preorder α] {f g : α → M₀} [PosMulMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : Monotone g) (hf₀ : ∀ (x : α), 0 ≤ f x) (hg₀ : ∀ (x : α), 0 ≤ g x) : Monotone (f * g)

theorem MonotoneOn.mul {α : Type u_1} {M₀ : Type u_2} [Mul M₀] [Zero M₀] [Preorder M₀] [Preorder α] {f g : α → M₀} [PosMulMono M₀] [MulPosMono M₀] {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) (hf₀ : ∀ (x : α), x ∈ s → 0 ≤ f x) (hg₀ : ∀ (x : α), x ∈ s → 0 ≤ g x) : MonotoneOn (f * g) s

@[simp]

theorem pow_succ_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (ha : 0 ≤ a) (n : ℕ) : 0 ≤ a ^ (n + 1)

@[simp]

theorem pow_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 0 ≤ a) (n : ℕ) : 0 ≤ a ^ n

theorem zero_pow_le_one {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] [ZeroLEOneClass M₀] (n : ℕ) : 0 ^ n ≤ 1

theorem pow_right_anti₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : Antitone fun (n : ℕ) => a ^ n

theorem pow_le_pow_of_le_one {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (hmn : m ≤ n) : a ^ n ≤ a ^ m

theorem pow_le_of_le_one {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : ℕ} [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) (hn : n ≠ 0) : a ^ n ≤ a

theorem sq_le {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a

theorem pow_le_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] {n : ℕ} (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : a ^ n ≤ 1

theorem one_le_mul_of_one_le_of_one_le {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

theorem one_lt_mul_of_le_of_lt {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

theorem one_lt_mul_of_lt_of_le {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

theorem one_lt_mul {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Alias of one_lt_mul_of_le_of_lt.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2026-07-28")]

theorem mul_lt_one_of_nonneg_of_lt_one_left {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) : a * b < 1

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2026-07-28")]

theorem mul_lt_one_of_nonneg_of_lt_one_right {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : a * b < 1

theorem Bound.one_lt_mul {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] : 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b

theorem Bound.mul_le_one {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [PosMulMono M₀] [MulPosMono M₀] (ha : a ≤ 1) (hb : b ≤ 1) : 0 ≤ a ∨ 0 ≤ b → a * b ≤ 1

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2026-07-28")]

theorem mul_le_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1

theorem pow_lt_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} : n ≠ 0 → a ^ n < 1

theorem pow_right_mono₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (h : 1 ≤ a) : Monotone fun (x : ℕ) => a ^ x

theorem one_le_pow₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) {n : ℕ} : 1 ≤ a ^ n

theorem one_lt_pow₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) {n : ℕ} : n ≠ 0 → 1 < a ^ n

theorem Bound.pow_le_pow_right_of_le_one_or_one_le {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {m n : ℕ} [ZeroLEOneClass M₀] [PosMulMono M₀] (h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) : a ^ n ≤ a ^ m

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

theorem pow_le_pow_right₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {m n : ℕ} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n

theorem le_self_pow₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n

theorem Bound.le_self_pow_of_pos {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : 0 < n) : a ≤ a ^ n

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

theorem pow_le_pow_left₀ {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a b : M₀} [PosMulMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n

theorem pow_left_monotoneOn {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {n : ℕ} [PosMulMono M₀] [MulPosMono M₀] : MonotoneOn (fun (a : M₀) => a ^ n) {x : M₀ | 0 ≤ x}

theorem monotone_mul_left_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (ha : 0 ≤ a) : Monotone fun (x : M₀) => a * x

theorem monotone_mul_right_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [MulPosMono M₀] (ha : 0 ≤ a) : Monotone fun (x : M₀) => x * a

theorem Monotone.mul_const {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : α → M₀} [MulPosMono M₀] (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun (x : α) => f x * a

theorem Monotone.const_mul {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : α → M₀} [PosMulMono M₀] (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun (x : α) => a * f x

theorem Antitone.mul_const {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : α → M₀} [MulPosMono M₀] (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun (x : α) => f x * a

theorem Antitone.const_mul {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [Preorder α] {f : α → M₀} [PosMulMono M₀] (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun (x : α) => a * f x

theorem mul_self_lt_mul_self {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a < b) : a * a < b * b

theorem strictMonoOn_mul_self {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] [PosMulStrictMono M₀] [MulPosMono M₀] : StrictMonoOn (fun (x : M₀) => x * x) {x : M₀ | 0 ≤ x}

theorem Decidable.mul_lt_mul'' {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a b c d : M₀} [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] [DecidableLE M₀] (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d

theorem lt_mul_left {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [MulPosStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < b * a

theorem lt_mul_right {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < a * b

theorem lt_mul_self {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) : a < a * a

theorem sq_pos_of_pos {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] (ha : 0 < a) : 0 < a ^ 2

@[simp]

theorem pow_succ_pos {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] (ha : 0 < a) (n : ℕ) : 0 < a ^ (n + 1)

@[simp]

theorem pow_pos {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] [ZeroLEOneClass M₀] (ha : 0 < a) (n : ℕ) : 0 < a ^ n

theorem pow_lt_pow_left₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀] [MulPosMono M₀] (hab : a < b) (ha : 0 ≤ a) {n : ℕ} : n ≠ 0 → a ^ n < b ^ n

theorem pow_left_strictMonoOn₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {n : ℕ} [PosMulStrictMono M₀] [MulPosMono M₀] (hn : n ≠ 0) : StrictMonoOn (fun (x : M₀) => x ^ n) {a : M₀ | 0 ≤ a}

See also pow_left_strictMono₀ and Nat.pow_left_strictMono.

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

See also pow_right_strictMono'.

theorem pow_lt_pow_right₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀] [ZeroLEOneClass M₀] (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n

theorem pow_lt_pow_iff_right₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀] [ZeroLEOneClass M₀] (h : 1 < a) : a ^ n < a ^ m ↔ n < m

theorem pow_le_pow_iff_right₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀] [ZeroLEOneClass M₀] (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m

theorem lt_self_pow₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m : ℕ} [PosMulStrictMono M₀] [ZeroLEOneClass M₀] (h : 1 < a) (hm : 1 < m) : a < a ^ m

theorem pow_right_strictAnti₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun (x : ℕ) => a ^ x

theorem pow_le_pow_iff_right_of_lt_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀] (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ m ≤ a ^ n ↔ n ≤ m

theorem pow_lt_pow_iff_right_of_lt_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m

theorem pow_lt_pow_right_of_lt_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

theorem pow_lt_self_of_lt_one₀ {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} {n : ℕ} [PosMulStrictMono M₀] (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a

theorem strictMono_mul_left_of_pos {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] (ha : 0 < a) : StrictMono fun (x : M₀) => a * x

theorem strictMono_mul_right_of_pos {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [MulPosStrictMono M₀] (ha : 0 < a) : StrictMono fun (x : M₀) => x * a

theorem StrictMono.mul_const {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : α → M₀} [MulPosStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) : StrictMono fun (x : α) => f x * a

theorem StrictMono.const_mul {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : α → M₀} [PosMulStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) : StrictMono fun (x : α) => a * f x

theorem StrictAnti.mul_const {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : α → M₀} [MulPosStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun (x : α) => f x * a

theorem StrictAnti.const_mul {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [Preorder α] {f : α → M₀} [PosMulStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun (x : α) => a * f x

theorem StrictMono.mul_monotone {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] [Preorder α] {f g : α → M₀} [PosMulMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : Monotone g) (hf₀ : ∀ (x : α), 0 ≤ f x) (hg₀ : ∀ (x : α), 0 < g x) : StrictMono (f * g)

theorem Monotone.mul_strictMono {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] [Preorder α] {f g : α → M₀} [PosMulStrictMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : StrictMono g) (hf₀ : ∀ (x : α), 0 < f x) (hg₀ : ∀ (x : α), 0 ≤ g x) : StrictMono (f * g)

theorem StrictMono.mul {α : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] [Preorder α] {f g : α → M₀} [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : StrictMono g) (hf₀ : ∀ (x : α), 0 ≤ f x) (hg₀ : ∀ (x : α), 0 ≤ g x) : StrictMono (f * g)

theorem pow_le_pow_iff_left₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ} [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem pow_lt_pow_iff_left₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ} [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

@[simp]

theorem pow_left_inj₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ} [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem pow_right_injective₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} [ZeroLEOneClass M₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Function.Injective fun (x : ℕ) => a ^ x

@[simp]

theorem pow_right_inj₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {m n : ℕ} [ZeroLEOneClass M₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

theorem pow_le_one_iff_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

theorem one_le_pow_iff_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] (ha : 0 ≤ a) (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a

theorem pow_lt_one_iff_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n < 1 ↔ a < 1

theorem one_lt_pow_iff_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] (ha : 0 ≤ a) (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a

theorem pow_eq_one_iff_of_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀] (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1

theorem sq_le_one_iff₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} [ZeroLEOneClass M₀] (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1

theorem sq_lt_one_iff₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} [ZeroLEOneClass M₀] (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1

theorem one_le_sq_iff₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} [ZeroLEOneClass M₀] (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a

theorem one_lt_sq_iff₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} [ZeroLEOneClass M₀] (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a

theorem lt_of_pow_lt_pow_left₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀] (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b

theorem le_of_pow_le_pow_left₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ} [MulPosMono M₀] (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b

theorem sq_eq_sq₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b

theorem lt_of_mul_self_lt_mul_self₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀] (hb : 0 ≤ b) : a * a < b * b → a < b

theorem sq_lt_sq₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 < b ^ 2 ↔ a < b

theorem sq_le_sq₀ {M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b

theorem mul_inv_left_le {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (hb : 0 ≤ b) : a * (a⁻¹ * b) ≤ b

Equality holds when a ≠ 0. See mul_inv_cancel_left.

theorem le_mul_inv_left {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (hb : b ≤ 0) : b ≤ a * (a⁻¹ * b)

Equality holds when a ≠ 0. See mul_inv_cancel_left.

theorem inv_mul_left_le {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (hb : 0 ≤ b) : a⁻¹ * (a * b) ≤ b

Equality holds when a ≠ 0. See inv_mul_cancel_left.

theorem le_inv_mul_left {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (hb : b ≤ 0) : b ≤ a⁻¹ * (a * b)

Equality holds when a ≠ 0. See inv_mul_cancel_left.

theorem mul_inv_right_le {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (ha : 0 ≤ a) : a * b * b⁻¹ ≤ a

Equality holds when b ≠ 0. See mul_inv_cancel_right.

theorem le_mul_inv_right {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (ha : a ≤ 0) : a ≤ a * b * b⁻¹

Equality holds when b ≠ 0. See mul_inv_cancel_right.

theorem inv_mul_right_le {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (ha : 0 ≤ a) : a * b⁻¹ * b ≤ a

Equality holds when b ≠ 0. See inv_mul_cancel_right.

theorem le_inv_mul_right {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b : G₀} (ha : a ≤ 0) : a ≤ a * b⁻¹ * b

Equality holds when b ≠ 0. See inv_mul_cancel_right.

theorem mul_div_mul_right_le {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b c : G₀} (h : 0 ≤ a / b) : a * c / (b * c) ≤ a / b

Equality holds when c ≠ 0. See mul_div_mul_right.

theorem le_mul_div_mul_right {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] {a b c : G₀} (h : a / b ≤ 0) : a / b ≤ a * c / (b * c)

Equality holds when c ≠ 0. See mul_div_mul_right.

theorem div_self_le_one {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] [ZeroLEOneClass G₀] (a : G₀) : a / a ≤ 1

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

theorem mul_inv_le_one {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] [ZeroLEOneClass G₀] {a : G₀} : a * a⁻¹ ≤ 1

Equality holds when a ≠ 0. See mul_inv_cancel.

theorem inv_mul_le_one {G₀ : Type u_3} [GroupWithZero G₀] [Preorder G₀] [ZeroLEOneClass G₀] {a : G₀} : a⁻¹ * a ≤ 1

Equality holds when a ≠ 0. See inv_mul_cancel.

@[simp]

theorem inv_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} : 0 < a⁻¹ ↔ 0 < a

theorem inv_pos_of_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} : 0 < a → 0 < a⁻¹

Alias of the reverse direction of inv_pos.

@[simp]

theorem inv_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} : 0 ≤ a⁻¹ ↔ 0 ≤ a

theorem inv_nonneg_of_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} : 0 ≤ a → 0 ≤ a⁻¹

Alias of the reverse direction of inv_nonneg.

theorem one_div_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} : 0 < 1 / a ↔ 0 < a

theorem one_div_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} : 0 ≤ 1 / a ↔ 0 ≤ a

theorem PosMulReflectLT.toPosMulStrictMono (G₀ : Type u_3) [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] : PosMulStrictMono G₀

For a group with zero, PosMulReflectLT G₀ implies PosMulStrictMono G₀.

theorem MulPosReflectLE.of_posMulReflectLT_of_mulPosMono (G₀ : Type u_3) [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] : MulPosReflectLE G₀

For a group with zero, PosMulReflectLT G₀ allows us to upgrade MulPosMono G₀ to MulPosReflectLE G₀. The other implication holds without the PosMulReflectLT G₀ assumption, see MulPosReflectLT.toMulPosStrictMono for a stronger version below.

This theorem shows that in the presence of the assumption PosMulReflectLT G₀, it makes no sense to optimize between assumptions MulPosMono G₀, MulPosStrictMono G₀, MulPosReflectLT G₀, and MulPosReflectLE G₀.

theorem div_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : 0 < a / b

theorem div_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b

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

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

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

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

theorem one_le_inv_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 < a) : 1 ≤ a⁻¹ * b ↔ a ≤ b

theorem inv_mul_le_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 < a) : a⁻¹ * b ≤ 1 ↔ b ≤ a

theorem inv_le_iff_one_le_mul₀' {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ a * b

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

theorem one_le_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) : 1 ≤ a⁻¹ ↔ a ≤ 1

theorem inv_le_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) : a⁻¹ ≤ 1 ↔ 1 ≤ a

theorem Bound.one_le_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) : a ≤ 1 → 1 ≤ a⁻¹

Alias of the reverse direction of one_le_inv₀.

theorem mul_le_of_le_inv_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c⁻¹ * b) : c * a ≤ b

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

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

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

theorem lt_inv_mul_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a < c⁻¹ * b ↔ c * a < b

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

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

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

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

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

theorem one_lt_inv_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 < a) : 1 < a⁻¹ * b ↔ a < b

theorem inv_mul_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} (ha : 0 < a) : a⁻¹ * b < 1 ↔ b < a

theorem one_lt_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) : 1 < a⁻¹ ↔ a < 1

theorem inv_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) : a⁻¹ < 1 ↔ 1 < a

theorem inv_lt_one_of_one_lt₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 1 < a) : a⁻¹ < 1

theorem one_lt_inv_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] : 1 < a⁻¹ ↔ 0 < a ∧ a < 1

theorem inv_le_one_of_one_le₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 1 ≤ a) : a⁻¹ ≤ 1

theorem one_le_inv_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1

theorem inv_mul_le_one_of_le₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : b⁻¹ * a ≤ 1

theorem zpow_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 0 ≤ a) (n : ℤ) : 0 ≤ a ^ n

theorem zpow_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 0 < a) (n : ℤ) : 0 < a ^ n

theorem zpow_right_mono₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 1 ≤ a) : Monotone fun (n : ℤ) => a ^ n

theorem zpow_right_anti₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha₀ : 0 < a) (ha₁ : a ≤ 1) : Antitone fun (n : ℤ) => a ^ n

theorem zpow_right_strictMono₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 1 < a) : StrictMono fun (n : ℤ) => a ^ n

theorem zpow_right_strictAnti₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha₀ : 0 < a) (ha₁ : a < 1) : StrictAnti fun (n : ℤ) => a ^ n

theorem zpow_le_zpow_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n

theorem zpow_le_zpow_right_of_le_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hmn : m ≤ n) : a ^ n ≤ a ^ m

theorem one_le_zpow₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 ≤ a) (hn : 0 ≤ n) : 1 ≤ a ^ n

theorem zpow_le_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : 0 ≤ n) : a ^ n ≤ 1

theorem zpow_le_one_of_nonpos₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 ≤ a) (hn : n ≤ 0) : a ^ n ≤ 1

theorem one_le_zpow_of_nonpos₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : n ≤ 0) : 1 ≤ a ^ n

theorem zpow_lt_zpow_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n

theorem zpow_lt_zpow_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

theorem one_lt_zpow₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n

theorem zpow_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) (hn : 0 < n) : a ^ n < 1

theorem zpow_lt_one_of_neg₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 < a) (hn : n < 0) : a ^ n < 1

theorem one_lt_zpow_of_neg₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) (hn : n < 0) : 1 < a ^ n

@[simp]

theorem zpow_le_zpow_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

@[simp]

theorem zpow_lt_zpow_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n

theorem zpow_le_zpow_iff_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ m ≤ a ^ n ↔ n ≤ m

theorem zpow_lt_zpow_iff_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {m n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ m < a ^ n ↔ n < m

@[simp]

theorem one_le_zpow_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 < a) : 1 ≤ a ^ n ↔ 0 ≤ n

@[simp]

theorem one_lt_zpow_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 < a) : 1 < a ^ n ↔ 0 < n

@[simp]

theorem one_le_zpow_iff_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) : 1 ≤ a ^ n ↔ n ≤ 0

@[simp]

theorem one_lt_zpow_iff_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) : 1 < a ^ n ↔ n < 0

@[simp]

theorem zpow_le_one_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 < a) : a ^ n ≤ 1 ↔ n ≤ 0

@[simp]

theorem zpow_lt_one_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha : 1 < a) : a ^ n < 1 ↔ n < 0

@[simp]

theorem zpow_le_one_iff_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n ≤ 1 ↔ 0 ≤ n

@[simp]

theorem zpow_lt_one_iff_right_of_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] {n : ℤ} (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n < 1 ↔ 0 < n

theorem zpow_left_monoOn₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {n : ℤ} (hn : 0 ≤ n) : MonotoneOn (fun (a : G₀) => a ^ n) {a : G₀ | 0 ≤ a}

theorem zpow_left_strictMonoOn₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {n : ℤ} (hn : 0 < n) : StrictMonoOn (fun (a : G₀) => a ^ n) {a : G₀ | 0 ≤ a}

theorem zpow_le_zpow_left₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] {n : ℤ} (hn : 0 ≤ n) (ha : 0 ≤ a) (h : a ≤ b) : a ^ n ≤ b ^ n

theorem zpow_lt_zpow_left₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀] {n : ℤ} (hn : 0 < n) (ha : 0 ≤ a) (h : a < b) : a ^ n < b ^ n

theorem Right.inv_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a : G₀} : 0 < a⁻¹ ↔ 0 < a

theorem MulPosReflectLT.toMulPosStrictMono (G₀ : Type u_3) [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] : MulPosStrictMono G₀

For a group with zero, MulPosReflectLT G₀ implies MulPosStrictMono G₀.

theorem Right.inv_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a : G₀} : 0 ≤ a⁻¹ ↔ 0 ≤ a

theorem div_nonpos_of_nonpos_of_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0

theorem le_mul_inv_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b

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

theorem mul_inv_le_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ a * c

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

theorem lt_mul_inv_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a < b * c⁻¹ ↔ a * c < b

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

theorem mul_inv_lt_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : b * c⁻¹ < a ↔ b < a * c

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

theorem le_div_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b

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

theorem div_le_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c

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

theorem lt_div_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a < b / c ↔ a * c < b

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

theorem div_lt_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : b / c < a ↔ b < a * c

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

theorem div_le_div_iff_of_pos_right {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b

theorem div_lt_div_iff_of_pos_right {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a / c < b / c ↔ a < b

theorem inv_le_iff_one_le_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ b * a

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

theorem inv_lt_iff_one_lt_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) : a⁻¹ < b ↔ 1 < b * a

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

theorem one_le_div₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

theorem one_lt_div₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (hb : 0 < b) : 1 < a / b ↔ b < a

theorem div_le_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b

theorem div_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} (hb : 0 < b) : a / b < 1 ↔ a < b

theorem mul_le_of_le_mul_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c⁻¹) : a * c ≤ b

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

theorem mul_inv_le_of_le_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a * b⁻¹ ≤ c

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

theorem mul_le_of_le_div₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b / c) : a * c ≤ b

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

theorem div_le_of_le_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c

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

theorem mul_inv_le_one_of_le₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1

theorem div_le_one_of_le₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀} [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1

theorem div_le_div_of_nonneg_right {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c

theorem div_lt_div_of_pos_right {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀} (h : a < b) (hc : 0 < c) : a / c < b / c

theorem inv_le_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

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

theorem inv_lt_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b⁻¹ ↔ b < a

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

theorem inv_anti₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (hb : 0 < b) (hba : b ≤ a) : a⁻¹ ≤ b⁻¹

theorem inv_strictAnti₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (hb : 0 < b) (hba : b < a) : a⁻¹ < b⁻¹

theorem strictAntiOn_inv_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] : StrictAntiOn (fun (x : G₀) => x⁻¹) {r : G₀ | 0 < r}

theorem antitoneOn_inv_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] : AntitoneOn (fun (x : G₀) => x⁻¹) {r : G₀ | 0 < r}

theorem inv_le_comm₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

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

theorem inv_lt_comm₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a

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

theorem inv_le_of_inv_le₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (h : a⁻¹ ≤ b) : b⁻¹ ≤ a

theorem inv_lt_of_inv_lt₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (h : a⁻¹ < b) : b⁻¹ < a

theorem le_inv_comm₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹

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

theorem lt_inv_comm₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹

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

theorem le_inv_of_le_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (h : a ≤ b⁻¹) : b ≤ a⁻¹

theorem lt_inv_of_lt_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b : G₀} (ha : 0 < a) (h : a < b⁻¹) : b < a⁻¹

theorem div_le_div_iff_of_pos_left {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c : G₀} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b

theorem div_lt_div_iff_of_pos_left {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c : G₀} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b < a / c ↔ c < b

theorem div_le_div_of_nonneg_left {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c : G₀} (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c

theorem div_lt_div_of_pos_left {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c : G₀} (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c

theorem div_le_div₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c d : G₀} (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d

theorem div_lt_div₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c d : G₀} (hac : a < c) (hdb : d ≤ b) (hc : 0 ≤ c) (hd : 0 < d) : a / b < c / d

theorem div_lt_div₀' {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] {a b c d : G₀} (hac : a ≤ c) (hdb : d < b) (hc : 0 < c) (hd : 0 < d) : a / b < c / d

@[simp]

theorem inv_neg'' {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] : a⁻¹ < 0 ↔ a < 0

@[simp]

theorem inv_nonpos {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] : a⁻¹ ≤ 0 ↔ a ≤ 0

theorem inv_lt_zero {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] : a⁻¹ < 0 ↔ a < 0

Alias of inv_neg''.

theorem one_div_neg {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] : 1 / a < 0 ↔ a < 0

theorem one_div_nonpos {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] : 1 / a ≤ 0 ↔ a ≤ 0

theorem div_nonpos_of_nonneg_of_nonpos {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a b : G₀} [PosMulMono G₀] (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0

theorem neg_of_div_neg_right {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a b : G₀} [PosMulMono G₀] (h : a / b < 0) (ha : 0 ≤ a) : b < 0

theorem neg_of_div_neg_left {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a b : G₀} [PosMulMono G₀] (h : a / b < 0) (hb : 0 ≤ b) : a < 0

theorem inv_lt_one_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀] [ZeroLEOneClass G₀] : a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

theorem inv_le_one_iff₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀] [ZeroLEOneClass G₀] : a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

theorem zpow_right_injective₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀] [ZeroLEOneClass G₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Function.Injective fun (n : ℤ) => a ^ n

@[simp]

theorem zpow_right_inj₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} {m n : ℤ} [PosMulStrictMono G₀] [ZeroLEOneClass G₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

theorem zpow_eq_one_iff_right₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀] [ZeroLEOneClass G₀] (ha₀ : 0 ≤ a) (ha₁ : a ≠ 1) {n : ℤ} : a ^ n = 1 ↔ n = 0

theorem zpow_le_zpow_iff_left₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a b : G₀} {n : ℤ} [PosMulReflectLT G₀] [MulPosMono G₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < n) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem zpow_lt_zpow_iff_left₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a b : G₀} {n : ℤ} [PosMulReflectLT G₀] [MulPosMono G₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < n) : a ^ n < b ^ n ↔ a < b

theorem zpow_left_injOn₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] [PosMulStrictMono G₀] [MulPosMono G₀] {n : ℤ} : n ≠ 0 → Set.InjOn (fun (a : G₀) => a ^ n) {a : G₀ | 0 ≤ a}

theorem zpow_left_inj₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a b : G₀} {n : ℤ} [PosMulStrictMono G₀] [MulPosMono G₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem mul_div_mul_left_le {G₀ : Type u_3} [CommGroupWithZero G₀] [Preorder G₀] {a b c : G₀} (h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b

Equality holds when c ≠ 0. See mul_div_mul_left.

theorem le_mul_div_mul_left {G₀ : Type u_3} [CommGroupWithZero G₀] [Preorder G₀] {a b c : G₀} (h : a / b ≤ 0) : a / b ≤ c * a / (c * b)

Equality holds when c ≠ 0. See mul_div_mul_left.

theorem le_inv_mul_iff₀' {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a ≤ c⁻¹ * b ↔ a * c ≤ b

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

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

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

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

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

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

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

theorem div_le_div_iff₀ {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c d : G₀} (hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b

theorem le_div_iff₀' {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b

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

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

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

theorem le_div_comm₀ {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (ha : 0 < a) (hc : 0 < c) : a ≤ b / c ↔ c ≤ b / a

theorem div_le_comm₀ {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hb : 0 < b) (hc : 0 < c) : a / b ≤ c ↔ a / c ≤ b

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

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

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

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

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

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

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

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

theorem div_lt_div_iff₀ {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c d : G₀} (hb : 0 < b) (hd : 0 < d) : a / b < c / d ↔ a * d < c * b

theorem lt_div_iff₀' {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hc : 0 < c) : a < b / c ↔ c * a < b

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

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

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

theorem lt_div_comm₀ {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (ha : 0 < a) (hc : 0 < c) : a < b / c ↔ c < b / a

theorem div_lt_comm₀ {G₀ : Type u_3} [CommGroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀} (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b