Documentation

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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.

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

Assumes left covariance.

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

source
theorem mul_neg_of_pos_of_neg {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) :
a * b < 0
source
@[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
source
theorem Right.mul_pos {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosStrictMono α] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Assumes right covariance.

source
theorem mul_neg_of_neg_of_pos {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) :
a * b < 0
source
@[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
source
theorem Left.mul_nonneg {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a * b

Assumes left covariance.

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

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

Assumes right covariance.

source
theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) :
a * b ≤ 0
source
theorem pos_of_mul_pos_right {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulReflectLT α] (h : 0 < a * b) (ha : 0 ≤ a) :
0 < b
source
theorem pos_of_mul_pos_left {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [MulPosReflectLT α] (h : 0 < a * b) (hb : 0 ≤ b) :
0 < a
source
theorem pos_iff_pos_of_mul_pos {α : Type u_1} [MulZeroClass α] {a b : α} [Preorder α] [PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) :
0 < a ↔ 0 < b
source
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.

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

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

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

source
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
source
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
source
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
source
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
source
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
source
@[instance 100]
instance PosMulStrictMono.toPosMulMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] :
PosMulMono α
source
@[instance 100]
instance MulPosStrictMono.toMulPosMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [MulPosStrictMono α] :
MulPosMono α
source
@[instance 100]
instance PosMulReflectLE.toPosMulReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [PosMulReflectLE α] :
PosMulReflectLT α
source
@[instance 100]
instance MulPosReflectLE.toMulPosReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [MulPosReflectLE α] :
MulPosReflectLT α
source
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
source
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
source
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
source
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
source
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
source
theorem neg_of_mul_pos_right {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a ≤ 0) :
b < 0
source
theorem neg_of_mul_pos_left {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b ≤ 0) :
a < 0
source
theorem neg_iff_neg_of_mul_pos {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
a < 0 ↔ b < 0
source
theorem Left.neg_of_mul_neg_right {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] (h : a * b < 0) (a0 : 0 ≤ a) :
b < 0
source
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.

source
theorem Right.neg_of_mul_neg_right {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [MulPosMono α] (h : a * b < 0) (a0 : 0 ≤ a) :
b < 0
source
theorem Left.neg_of_mul_neg_left {α : Type u_1} [MulZeroClass α] {a b : α} [LinearOrder α] [PosMulMono α] (h : a * b < 0) (b0 : 0 ≤ b) :
a < 0
source
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.

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

source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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.

source
@[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
source
@[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
source
@[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
source
@[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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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
source
@[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)
source
@[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
source
theorem zero_pow_le_one {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] [ZeroLEOneClass M₀] (n : ℕ) :
0 ^ n ≤ 1
source
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
source
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
source
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
source
theorem sq_le {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) :
a ^ 2 ≤ a
source
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
source
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
source
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
source
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
source
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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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

source
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
source
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
source
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

source
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
source
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}
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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}
source
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
source
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
source
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
source
theorem lt_mul_self {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) :
a < a * a
source
theorem sq_pos_of_pos {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀] (ha : 0 < a) :
0 < a ^ 2
source
@[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)
source
@[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
source
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
source
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.

source
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'.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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
source
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
source
@[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
source
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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem PosMulMono.toPosMulStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [PosMulMono α] :
PosMulStrictMono α
source
theorem posMulMono_iff_posMulStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] :
PosMulMono α ↔ PosMulStrictMono α
source
theorem MulPosMono.toMulPosStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [MulPosMono α] :
MulPosStrictMono α
source
theorem mulPosMono_iff_mulPosStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] :
MulPosMono α ↔ MulPosStrictMono α
source
theorem PosMulReflectLT.toPosMulReflectLE {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [PosMulReflectLT α] :
PosMulReflectLE α
source
theorem posMulReflectLE_iff_posMulReflectLT {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] :
PosMulReflectLE α ↔ PosMulReflectLT α
source
theorem MulPosReflectLT.toMulPosReflectLE {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [MulPosReflectLT α] :
MulPosReflectLE α
source
theorem mulPosReflectLE_iff_mulPosReflectLT {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] :
MulPosReflectLE α ↔ MulPosReflectLT α
source
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.

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

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

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

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

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

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

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

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

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

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

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

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

source
@[simp]
theorem inv_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} :
0 < a⁻¹ ↔ 0 < a
source
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.

source
@[simp]
theorem inv_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} :
0 ≤ a⁻¹ ↔ 0 ≤ a
source
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.

source
theorem one_div_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} :
0 < 1 / a ↔ 0 < a
source
theorem one_div_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} :
0 ≤ 1 / a ↔ 0 ≤ a
source
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₀.

source
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₀.

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

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

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

source
theorem one_le_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) :
1 ≤ a⁻¹ ↔ a ≤ 1
source
theorem inv_le_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) :
a⁻¹ ≤ 1 ↔ 1 ≤ a
source
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₀.

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

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

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

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

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

source
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
source
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
source
theorem one_lt_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) :
1 < a⁻¹ ↔ a < 1
source
theorem inv_lt_one₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} (ha : 0 < a) :
a⁻¹ < 1 ↔ 1 < a
source
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
source
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
source
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
source
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
source
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
source
theorem zpow_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 0 ≤ a) (n : ℤ) :
0 ≤ a ^ n
source
theorem zpow_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀] (ha : 0 < a) (n : ℤ) :
0 < a ^ n
source
theorem zpow_left_strictMonoOn₀ {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] {n : ℤ} [MulPosMono G₀] (hn : 0 < n) :
StrictMonoOn (fun (a : G₀) => a ^ n) {a : G₀ | 0 ≤ a}
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem Right.inv_pos {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a : G₀} :
0 < a⁻¹ ↔ 0 < a
source
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₀.

source
theorem Right.inv_nonneg {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] {a : G₀} :
0 ≤ a⁻¹ ↔ 0 ≤ a
source
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
source
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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
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⁻¹
source
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⁻¹
source
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.

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

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

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

source
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⁻¹
source
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⁻¹
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem inv_neg'' {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] :
a⁻¹ < 0 ↔ a < 0
source
@[simp]
theorem inv_nonpos {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] :
a⁻¹ ≤ 0 ↔ a ≤ 0
source
theorem inv_lt_zero {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] :
a⁻¹ < 0 ↔ a < 0

Alias of inv_neg''.

source
theorem one_div_neg {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] :
1 / a < 0 ↔ a < 0
source
theorem one_div_nonpos {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulMono G₀] :
1 / a ≤ 0 ↔ a ≤ 0
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem zpow_right_inj₀ {G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀] {m n : ℤ} [ZeroLEOneClass G₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) :
a ^ m = a ^ n ↔ m = n
source
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
source
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.

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

source
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 ↔ c * a ≤ b

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

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

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

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

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

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

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

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

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

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

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

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

source
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
source
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