Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Left.one_le_pow_of_le theorem

(ha : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n

Full source

@[to_additive Left.nsmul_nonneg]
theorem one_le_pow_of_le (ha : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n
  | 0 => by simp
  | k + 1 => by
    rw [pow_succ]
    exact one_le_mul (one_le_pow_of_le ha k) ha

Monotonicity of Powers: $1 \leq a$ implies $1 \leq a^n$ for all $n \in \mathbb{N}$

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $1 \leq a$, then for all natural numbers $n$, we have $1 \leq a^n$.

Left.pow_le_one_of_le theorem

(ha : a ≤ 1) (n : ℕ) : a ^ n ≤ 1

Full source

@[to_additive nsmul_nonpos]
theorem pow_le_one_of_le (ha : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 := one_le_pow_of_le (M := Mᵒᵈ) ha n

Monotonicity of Powers: $a \leq 1$ implies $a^n \leq 1$ for all $n \in \mathbb{N}$

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $a \leq 1$, then for any natural number $n$, we have $a^n \leq 1$.

Left.pow_lt_one_of_lt theorem

{a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1

Full source

@[to_additive nsmul_neg]
theorem pow_lt_one_of_lt {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1 := by
  rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
  rw [pow_succ']
  exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

Strict Inequality for Powers: $a < 1$ implies $a^n < 1$ for $n \neq 0$

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $a < 1$ and $n$ is a nonzero natural number, then $a^n < 1$.

pow_right_monotone theorem

(ha : 1 ≤ a) : Monotone fun n : ℕ ↦ a ^ n

Full source

@[to_additive nsmul_left_monotone]
theorem pow_right_monotone (ha : 1 ≤ a) : Monotone fun n : ℕ ↦ a ^ n :=
  monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact le_mul_of_one_le_right' ha

Monotonicity of Powers for $a \geq 1$: $n \mapsto a^n$ is increasing

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $1 \leq a$, then the function $n \mapsto a^n$ is monotone. That is, for any natural numbers $n \leq m$, we have $a^n \leq a^m$.

pow_le_pow_right' theorem

{n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m

Full source

@[to_additive (attr := gcongr) nsmul_le_nsmul_left]
theorem pow_le_pow_right' {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
  pow_right_monotone ha h

Monotonicity of Powers: $1 \leq a$ and $n \leq m$ implies $a^n \leq a^m$

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $1 \leq a$ and $n \leq m$ are natural numbers, then $a^n \leq a^m$.

pow_le_pow_right_of_le_one' theorem

{n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n

Full source

@[to_additive nsmul_le_nsmul_left_of_nonpos]
theorem pow_le_pow_right_of_le_one' {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
  pow_le_pow_right' (M := Mᵒᵈ) ha h

Antitonicity of Powers for $a \leq 1$: $n \leq m$ implies $a^m \leq a^n$

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $a \leq 1$ and $n \leq m$ are natural numbers, then $a^m \leq a^n$.

one_lt_pow' theorem

(ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k

Full source

@[to_additive nsmul_pos]
theorem one_lt_pow' (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k :=
  pow_lt_one' (M := Mᵒᵈ) ha hk

One is Less Than Positive Power of Element Greater Than One

Informal description

For any element $a$ in a monoid $M$ with a preorder and left-monotone multiplication, if $1 < a$ and $k$ is a nonzero natural number, then $1 < a^k$.

le_self_pow theorem

(ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n

Full source

@[to_additive]
lemma le_self_pow (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n := by
  simpa using pow_le_pow_right' ha (Nat.one_le_iff_ne_zero.2 hn)

Element Bounded by Its Own Power: $a \leq a^n$ when $1 \leq a$ and $n \neq 0$

Informal description

For any element $a$ in a monoid $M$ with a preorder, if $1 \leq a$ and $n$ is a nonzero natural number, then $a \leq a^n$.

pow_right_strictMono' theorem

(ha : 1 < a) : StrictMono ((a ^ ·) : ℕ → M)

Full source

@[to_additive nsmul_left_strictMono]
theorem pow_right_strictMono' (ha : 1 < a) : StrictMono ((a ^ ·) : ℕ → M) :=
  strictMono_nat_of_lt_succ fun n ↦ by rw [pow_succ]; exact lt_mul_of_one_lt_right' (a ^ n) ha

Strict Monotonicity of Powers: $n \mapsto a^n$ is strictly increasing when $1 < a$

Informal description

For any element $a$ in a monoid $M$ with a preorder such that $1 < a$, the function $n \mapsto a^n$ is strictly increasing on the natural numbers $\mathbb{N}$.

pow_lt_pow_right' theorem

(ha : 1 < a) (h : n < m) : a ^ n < a ^ m

Full source

@[to_additive (attr := gcongr) nsmul_lt_nsmul_left]
theorem pow_lt_pow_right' (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
  pow_right_strictMono' ha h

Strict Monotonicity of Powers: $a^n < a^m$ when $1 < a$ and $n < m$

Informal description

For any element $a$ in a monoid $M$ with a preorder such that $1 < a$, and for any natural numbers $n < m$, we have $a^n < a^m$.

Right.one_le_pow_of_le theorem

(hx : 1 ≤ x) : ∀ {n : ℕ}, 1 ≤ x ^ n

Full source

@[to_additive Right.nsmul_nonneg]
theorem Right.one_le_pow_of_le (hx : 1 ≤ x) : ∀ {n : ℕ}, 1 ≤ x ^ n
  | 0 => (pow_zero _).ge
  | n + 1 => by
    rw [pow_succ]
    exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

Monotonicity of Powers: $1 \leq x$ implies $1 \leq x^n$ for all $n \in \mathbb{N}$

Informal description

For any element $x$ in a monoid $M$ with a preorder such that right multiplication is monotone, if $1 \leq x$, then for any natural number $n$, we have $1 \leq x^n$.

Right.pow_le_one_of_le theorem

(hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1

Full source

@[to_additive Right.nsmul_nonpos]
theorem Right.pow_le_one_of_le (hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1 :=
  Right.one_le_pow_of_le (M := Mᵒᵈ) hx

Monotonicity of Powers: $x \leq 1$ implies $x^n \leq 1$ for all $n \in \mathbb{N}$

Informal description

For any element $x$ in a monoid $M$ with a preorder such that right multiplication is monotone, if $x \leq 1$, then for any natural number $n$, we have $x^n \leq 1$.

Right.pow_lt_one_of_lt theorem

{n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1

Full source

@[to_additive Right.nsmul_neg]
theorem Right.pow_lt_one_of_lt {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1 := by
  rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩
  rw [pow_succ]
  exact mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h

Strict Inequality for Powers: $x < 1$ implies $x^n < 1$ for $n > 0$

Informal description

Let $M$ be a monoid with a preorder such that right multiplication is monotone. For any element $x \in M$ and natural number $n > 0$, if $x < 1$, then $x^n < 1$.

pow_le_pow_mul_of_sq_le_mul theorem

[MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b * a) : ∀ {n}, n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a

Full source

/-- This lemma is useful in non-cancellative monoids, like sets under pointwise operations. -/
@[to_additive
"This lemma is useful in non-cancellative monoids, like sets under pointwise operations."]
lemma pow_le_pow_mul_of_sq_le_mul [MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b * a) :
    ∀ {n}, n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a
  | 1, _ => by simp
  | n + 2, _ => by
    calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := mul_le_mul_right' (pow_le_pow_mul_of_sq_le_mul hab (by omega)) _
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := mul_le_mul_left' hab _
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]

Power Inequality in Monoids: $a^n \leq b^{n-1} \cdot a$ under $a^2 \leq b \cdot a$

Informal description

Let $M$ be a monoid with a preorder such that left multiplication is monotone. For any elements $a, b \in M$ satisfying $a^2 \leq b \cdot a$, and for any natural number $n \neq 0$, we have $a^n \leq b^{n-1} \cdot a$.

StrictMono.pow_const theorem

(hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono (f · ^ n)

Full source

@[to_additive StrictMono.const_nsmul]
theorem StrictMono.pow_const (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono (f · ^ n)
  | 0, hn => (hn rfl).elim
  | 1, _ => by simpa
  | Nat.succ <| Nat.succ n, _ => by
    simpa only [pow_succ] using (hf.pow_const n.succ_ne_zero).mul' hf

Strict Monotonicity of Powers of Strictly Monotone Functions

Informal description

Let $f : \alpha \to M$ be a strictly monotone function from a preorder $\alpha$ to a monoid $M$ with a strict order. For any natural number $n \neq 0$, the function $x \mapsto (f(x))^n$ is strictly monotone.

pow_left_strictMono theorem

(hn : n ≠ 0) : StrictMono (· ^ n : M → M)

Full source

/-- See also `pow_left_strictMonoOn₀`. -/
@[to_additive nsmul_right_strictMono]
theorem pow_left_strictMono (hn : n ≠ 0) : StrictMono (· ^ n : M → M) := strictMono_id.pow_const hn

Strict Monotonicity of Power Function: $x^n$ is strictly increasing for $n \neq 0$

Informal description

For any monoid $M$ with a strict order $<$ and any nonzero natural number $n$, the function $x \mapsto x^n$ is strictly monotone. That is, for any $a, b \in M$, if $a < b$ then $a^n < b^n$.

pow_lt_pow_left' theorem

(hn : n ≠ 0) {a b : M} (hab : a < b) : a ^ n < b ^ n

Full source

@[to_additive (attr := mono, gcongr) nsmul_lt_nsmul_right]
lemma pow_lt_pow_left' (hn : n ≠ 0) {a b : M} (hab : a < b) : a ^ n < b ^ n :=
  pow_left_strictMono hn hab

Strict Monotonicity of Powers: $a < b \implies a^n < b^n$ for $n \neq 0$

Informal description

For any monoid $M$ with a strict order $<$ and any nonzero natural number $n$, if $a < b$ for elements $a, b \in M$, then $a^n < b^n$.

pow_le_pow_left' theorem

{a b : M} (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i

Full source

@[to_additive (attr := mono, gcongr) nsmul_le_nsmul_right]
theorem pow_le_pow_left' {a b : M} (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i
  | 0 => by simp
  | k + 1 => by
    rw [pow_succ, pow_succ]
    exact mul_le_mul' (pow_le_pow_left' hab k) hab

Monotonicity of Powers: $a \leq b \implies a^i \leq b^i$ for all $i \in \mathbb{N}$

Informal description

For any elements $a$ and $b$ in a monoid $M$ with a preorder $\leq$, if $a \leq b$, then for every natural number $i$, the $i$-th power of $a$ is less than or equal to the $i$-th power of $b$, i.e., $a^i \leq b^i$.

Monotone.pow_const theorem

{f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n

Full source

@[to_additive Monotone.const_nsmul]
theorem Monotone.pow_const {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n
  | 0 => by simpa using monotone_const
  | n + 1 => by
    simp_rw [pow_succ]
    exact (Monotone.pow_const hf _).mul' hf

Monotonicity of Powers of Monotone Functions: $f$ monotone implies $f^n$ monotone for all $n \in \mathbb{N}$

Informal description

Let $M$ be a monoid with a preorder $\leq$, and let $f : \beta \to M$ be a monotone function. Then for every natural number $n$, the function $a \mapsto f(a)^n$ is also monotone. That is, for any $a, b \in \beta$, if $a \leq b$, then $f(a)^n \leq f(b)^n$.

pow_left_mono theorem

(n : ℕ) : Monotone fun a : M => a ^ n

Full source

@[to_additive nsmul_right_mono]
theorem pow_left_mono (n : ℕ) : Monotone fun a : M => a ^ n := monotone_id.pow_const _

Monotonicity of Power Function: $a \leq b \implies a^n \leq b^n$

Informal description

For any monoid $M$ with a preorder $\leq$ and any natural number $n$, the function $a \mapsto a^n$ is monotone. That is, for any $a, b \in M$, if $a \leq b$, then $a^n \leq b^n$.

pow_le_pow theorem

{a b : M} (hab : a ≤ b) (ht : 1 ≤ b) {m n : ℕ} (hmn : m ≤ n) : a ^ m ≤ b ^ n

Full source

@[to_additive (attr := gcongr)]
lemma pow_le_pow {a b : M} (hab : a ≤ b) (ht : 1 ≤ b) {m n : ℕ} (hmn : m ≤ n) : a ^ m ≤ b ^ n :=
  (pow_le_pow_left' hab _).trans (pow_le_pow_right' ht hmn)

Monotonicity of Powers: $a \leq b$ and $1 \leq b$ implies $a^m \leq b^n$ for $m \leq n$

Informal description

Let $M$ be a monoid with a preorder $\leq$. For any elements $a, b \in M$ such that $a \leq b$ and $1 \leq b$, and for any natural numbers $m, n$ with $m \leq n$, we have $a^m \leq b^n$.

le_pow_sup theorem

: a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n

Full source

lemma le_pow_sup : a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n :=
  sup_le (pow_le_pow_left' le_sup_left _) (pow_le_pow_left' le_sup_right _)

Supremum of Powers is Bounded by Power of Supremum: $a^n \sqcup b^n \leq (a \sqcup b)^n$

Informal description

For any elements $a$ and $b$ in a monoid $M$ equipped with a join-semilattice structure, and for any natural number $n$, the supremum of the $n$-th powers of $a$ and $b$ is less than or equal to the $n$-th power of their supremum, i.e., $a^n \sqcup b^n \leq (a \sqcup b)^n$.

pow_inf_le theorem

: (a ⊓ b) ^ n ≤ a ^ n ⊓ b ^ n

Full source

lemma pow_inf_le : (a ⊓ b) ^ n ≤ a ^ n ⊓ b ^ n :=
  le_inf (pow_le_pow_left' inf_le_left _) (pow_le_pow_left' inf_le_right _)

Power of Infimum is Bounded by Infimum of Powers: $(a \sqcap b)^n \leq a^n \sqcap b^n$

Informal description

For any elements $a$ and $b$ in a meet-semilattice with a monoid structure, and for any natural number $n$, the $n$-th power of the infimum $a \sqcap b$ is less than or equal to the infimum of the $n$-th powers of $a$ and $b$, i.e., $(a \sqcap b)^n \leq a^n \sqcap b^n$.

one_le_pow_iff theorem

{x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x

Full source

@[to_additive nsmul_nonneg_iff]
theorem one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x :=
  ⟨le_imp_le_of_lt_imp_lt fun h => pow_lt_one' h hn, fun h => one_le_pow_of_one_le' h n⟩

Characterization of $1 \leq x^n$ in Monoids: $1 \leq x^n \leftrightarrow 1 \leq x$ for $n \neq 0$

Informal description

For any element $x$ in a monoid $M$ and any nonzero natural number $n$, the inequality $1 \leq x^n$ holds if and only if $1 \leq x$.

pow_le_one_iff theorem

{x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1

Full source

@[to_additive]
theorem pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 :=
  one_le_pow_iff (M := Mᵒᵈ) hn

Characterization of $x^n \leq 1$ in Monoids: $x^n \leq 1 \leftrightarrow x \leq 1$ for $n \neq 0$

Informal description

For any element $x$ in a monoid $M$ and any nonzero natural number $n$, the inequality $x^n \leq 1$ holds if and only if $x \leq 1$.

one_lt_pow_iff theorem

{x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x

Full source

@[to_additive nsmul_pos_iff]
theorem one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x :=
  lt_iff_lt_of_le_iff_le (pow_le_one_iff hn)

Characterization of $1 < x^n$ in Monoids: $1 < x^n \leftrightarrow 1 < x$ for $n \neq 0$

Informal description

For any element $x$ in a monoid $M$ and any nonzero natural number $n$, the strict inequality $1 < x^n$ holds if and only if $1 < x$.

pow_lt_one_iff theorem

{x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1

Full source

@[to_additive]
theorem pow_lt_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1 :=
  lt_iff_lt_of_le_iff_le (one_le_pow_iff hn)

Characterization of $x^n < 1$ in Monoids: $x^n < 1 \leftrightarrow x < 1$ for $n \neq 0$

Informal description

For any element $x$ in a monoid $M$ and any nonzero natural number $n$, the inequality $x^n < 1$ holds if and only if $x < 1$.

pow_eq_one_iff theorem

{x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1

Full source

@[to_additive]
theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 := by
  simp only [le_antisymm_iff]
  rw [pow_le_one_iff hn, one_le_pow_iff hn]

Characterization of $x^n = 1$ in Monoids: $x^n = 1 \leftrightarrow x = 1$ for $n \neq 0$

Informal description

For any element $x$ in a monoid $M$ and any nonzero natural number $n$, the equality $x^n = 1$ holds if and only if $x = 1$.

pow_le_pow_iff_right' theorem

(ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

Full source

@[to_additive nsmul_le_nsmul_iff_left]
theorem pow_le_pow_iff_right' (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
  (pow_right_strictMono' ha).le_iff_le

Monotonicity of Powers: $a^m \leq a^n \leftrightarrow m \leq n$ when $1 < a$

Informal description

For any element $a$ in a monoid $M$ with a linear order such that $1 < a$, and for any natural numbers $m$ and $n$, the inequality $a^m \leq a^n$ holds if and only if $m \leq n$.

pow_lt_pow_iff_right' theorem

(ha : 1 < a) : a ^ m < a ^ n ↔ m < n

Full source

@[to_additive nsmul_lt_nsmul_iff_left]
theorem pow_lt_pow_iff_right' (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
  (pow_right_strictMono' ha).lt_iff_lt

Strict Monotonicity of Powers: $a^m < a^n \leftrightarrow m < n$ when $1 < a$

Informal description

For any element $a$ in a monoid $M$ with a linear order such that $1 < a$, and for any natural numbers $m$ and $n$, the inequality $a^m < a^n$ holds if and only if $m < n$.

lt_of_pow_lt_pow_left' theorem

{a b : M} (n : ℕ) : a ^ n < b ^ n → a < b

Full source

@[to_additive lt_of_nsmul_lt_nsmul_right]
theorem lt_of_pow_lt_pow_left' {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b :=
  (pow_left_mono _).reflect_lt

Strict inequality preserved under powers: $a^n < b^n \implies a < b$

Informal description

Let $M$ be a monoid with a linear order such that multiplication is monotone in both arguments. For any elements $a, b \in M$ and natural number $n$, if $a^n < b^n$, then $a < b$.

min_lt_of_mul_lt_sq theorem

{a b c : M} (h : a * b < c ^ 2) : min a b < c

Full source

@[to_additive min_lt_of_add_lt_two_nsmul]
theorem min_lt_of_mul_lt_sq {a b c : M} (h : a * b < c ^ 2) : min a b < c := by
  simpa using min_lt_max_of_mul_lt_mul (h.trans_eq <| pow_two _)

Minimum Bound from Product-Square Inequality: $\min(a,b) < c$ when $a \cdot b < c^2$

Informal description

For any elements $a, b, c$ in a monoid $M$ with a linear order and monotone multiplication, if the product $a \cdot b$ is strictly less than the square $c^2$, then the minimum of $a$ and $b$ is strictly less than $c$.

lt_max_of_sq_lt_mul theorem

{a b c : M} (h : a ^ 2 < b * c) : a < max b c

Full source

@[to_additive lt_max_of_two_nsmul_lt_add]
theorem lt_max_of_sq_lt_mul {a b c : M} (h : a ^ 2 < b * c) : a < max b c := by
  simpa using min_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)

Square-Strict-Multiplication Implies Less Than Maximum: $a^2 < b \cdot c \Rightarrow a < \max(b, c)$

Informal description

Let $M$ be a monoid with a linear order such that multiplication is both left-monotone and right-monotone. For any elements $a, b, c \in M$, if $a^2 < b \cdot c$, then $a$ is less than the maximum of $b$ and $c$, i.e., $a < \max(b, c)$.

le_of_pow_le_pow_left' theorem

{a b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b

Full source

@[to_additive le_of_nsmul_le_nsmul_right]
theorem le_of_pow_le_pow_left' {a b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b :=
  (pow_left_strictMono hn).le_iff_le.1

Strictly Monotone Power Implies Order: $a^n \leq b^n \Rightarrow a \leq b$ for $n \neq 0$

Informal description

Let $M$ be a monoid with a linear order such that multiplication is strictly monotone (both left and right). For any elements $a, b \in M$ and nonzero natural number $n$, if $a^n \leq b^n$, then $a \leq b$.

min_le_of_mul_le_sq theorem

{a b c : M} (h : a * b ≤ c ^ 2) : min a b ≤ c

Full source

@[to_additive min_le_of_add_le_two_nsmul]
theorem min_le_of_mul_le_sq {a b c : M} (h : a * b ≤ c ^ 2) : min a b ≤ c := by
  simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)

Minimum Bound from Product-Square Inequality: $\min(a, b) \leq c$ when $a \cdot b \leq c^2$

Informal description

For any elements $a, b, c$ in a monoid $M$ with strictly monotone multiplication (both left and right), if $a \cdot b \leq c^2$, then the minimum of $a$ and $b$ is less than or equal to $c$.

le_max_of_sq_le_mul theorem

{a b c : M} (h : a ^ 2 ≤ b * c) : a ≤ max b c

Full source

@[to_additive le_max_of_two_nsmul_le_add]
theorem le_max_of_sq_le_mul {a b c : M} (h : a ^ 2 ≤ b * c) : a ≤ max b c := by
  simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)

Maximum Bound from Square Inequality: $a^2 \leq b \cdot c \implies a \leq \max(b, c)$

Informal description

Let $M$ be a monoid with a linear order such that multiplication is both left and right strictly monotone. For any elements $a, b, c \in M$, if $a^2 \leq b \cdot c$, then $a \leq \max(b, c)$.

Left.pow_lt_one_iff' theorem

[MulLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1

Full source

@[to_additive Left.nsmul_neg_iff]
theorem Left.pow_lt_one_iff' [MulLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
    x ^ n < 1 ↔ x < 1 :=
  haveI := mulLeftMono_of_mulLeftStrictMono M
  pow_lt_one_iff hn.ne'

Strict Inequality for Powers under Left-Monotone Multiplication: $x^n < 1 \leftrightarrow x < 1$ for $n > 0$

Informal description

Let $M$ be a monoid with a linear order such that left multiplication is strictly monotone. For any element $x \in M$ and any positive natural number $n$, we have $x^n < 1$ if and only if $x < 1$.

Left.pow_lt_one_iff theorem

[MulLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1

Full source

theorem Left.pow_lt_one_iff [MulLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
    x ^ n < 1 ↔ x < 1 := Left.pow_lt_one_iff' hn

Strict Inequality for Powers under Left-Monotone Multiplication: $x^n < 1 \leftrightarrow x < 1$ for $n > 0$

Informal description

Let $M$ be a monoid with a linear order such that left multiplication is strictly monotone. For any element $x \in M$ and any positive natural number $n$, we have $x^n < 1$ if and only if $x < 1$.

Right.pow_lt_one_iff theorem

[MulRightStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1

Full source

@[to_additive]
theorem Right.pow_lt_one_iff [MulRightStrictMono M] {n : ℕ} {x : M}
    (hn : 0 < n) : x ^ n < 1 ↔ x < 1 :=
  haveI := mulRightMono_of_mulRightStrictMono M
  ⟨fun H => not_le.mp fun k => H.not_le <| Right.one_le_pow_of_le k, Right.pow_lt_one_of_lt hn⟩

Strict Inequality for Powers: $x^n < 1 \leftrightarrow x < 1$ for $n > 0$

Informal description

Let $M$ be a monoid with a strict right-monotone multiplication operation. For any natural number $n > 0$ and any element $x \in M$, we have $x^n < 1$ if and only if $x < 1$.

one_le_zpow theorem

{x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n

Full source

@[to_additive zsmul_nonneg]
theorem one_le_zpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n := by
  lift n to ℕ using hn
  rw [zpow_natCast]
  apply one_le_pow_of_one_le' H

Nonnegative integer powers preserve order from one

Informal description

Let $G$ be a division-inversion monoid. For any element $x \in G$ such that $1 \leq x$ and any integer $n \geq 0$, we have $1 \leq x^n$.