Documentation

Mathlib.Algebra.GroupPower.Order

Lemmas about the interaction of power operations with order #

Note that some lemmas are in Algebra/GroupPower/Lemmas.lean as they import files which depend on this file.

theorem nsmul_le_nsmul_of_le_right {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} {b : M} (hab : a b) (i : ) :
i a i b
abbrev nsmul_le_nsmul_of_le_right.match_1 (motive : Prop) :
(x : ) → (Unitmotive 0) → ((k : ) → motive (Nat.succ k)) → motive x
Equations
theorem pow_le_pow_of_le_left' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} {b : M} (hab : a b) (i : ) :
a ^ i b ^ i
theorem nsmul_nonneg {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} (H : 0 a) (n : ) :
0 n a
theorem one_le_pow_of_one_le' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} (H : 1 a) (n : ) :
1 a ^ n
theorem nsmul_nonpos {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} (H : a 0) (n : ) :
n a 0
theorem pow_le_one' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} (H : a 1) (n : ) :
a ^ n 1
theorem nsmul_le_nsmul {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} {n : } {m : } (ha : 0 a) (h : n m) :
n a m a
abbrev nsmul_le_nsmul.match_1 {n : } {m : } (motive : (k, n + k = m) → Prop) :
(x : k, n + k = m) → ((k : ) → (hk : n + k = m) → motive (_ : k, n + k = m)) → motive x
Equations
theorem pow_le_pow' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} {n : } {m : } (ha : 1 a) (h : n m) :
a ^ n a ^ m
theorem nsmul_le_nsmul_of_nonpos {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} {n : } {m : } (ha : a 0) (h : n m) :
m a n a
theorem pow_le_pow_of_le_one' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} {n : } {m : } (ha : a 1) (h : n m) :
a ^ m a ^ n
theorem nsmul_pos {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} (ha : 0 < a) {k : } (hk : k 0) :
0 < k a
theorem one_lt_pow' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} (ha : 1 < a) {k : } (hk : k 0) :
1 < a ^ k
theorem nsmul_neg {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : M} (ha : a < 0) {k : } (hk : k 0) :
k a < 0
theorem pow_lt_one' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : M} (ha : a < 1) {k : } (hk : k 0) :
a ^ k < 1
theorem nsmul_lt_nsmul {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {n : } {m : } (ha : 0 < a) (h : n < m) :
n a < m a
theorem pow_lt_pow' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} {n : } {m : } (ha : 1 < a) (h : n < m) :
a ^ n < a ^ m
theorem nsmul_strictMono_right {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} (ha : 0 < a) :
StrictMono ((fun x x_1 => x_1 x) a)
theorem pow_strictMono_left {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} (ha : 1 < a) :
StrictMono ((fun x x_1 => x ^ x_1) a)
theorem Left.pow_nonneg {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} (hx : 0 x) {n : } :
0 n x
theorem Left.one_le_pow_of_le {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} (hx : 1 x) {n : } :
1 x ^ n
theorem Left.pow_nonpos {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} (hx : x 0) {n : } :
n x 0
theorem Left.pow_le_one_of_le {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} (hx : x 1) {n : } :
x ^ n 1
theorem Right.pow_nonneg {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} (hx : 0 x) {n : } :
0 n x
theorem Right.one_le_pow_of_le {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} (hx : 1 x) {n : } :
1 x ^ n
theorem Right.pow_nonpos {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} (hx : x 0) {n : } :
n x 0
theorem Right.pow_le_one_of_le {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} (hx : x 1) {n : } :
x ^ n 1
theorem Left.pow_neg {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) (h : x < 0) :
n x < 0
theorem Left.pow_lt_one_of_lt {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) (h : x < 1) :
x ^ n < 1
theorem Right.pow_neg {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) (h : x < 0) :
n x < 0
theorem Right.pow_lt_one_of_lt {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) (h : x < 1) :
x ^ n < 1
theorem nsmul_nonneg_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
0 n x 0 x
theorem one_le_pow_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
1 x ^ n 1 x
theorem nsmul_nonpos_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
n x 0 x 0
theorem pow_le_one_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
x ^ n 1 x 1
theorem nsmul_pos_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
0 < n x 0 < x
theorem one_lt_pow_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
1 < x ^ n 1 < x
theorem nsmul_neg_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
n x < 0 x < 0
theorem pow_lt_one_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
x ^ n < 1 x < 1
theorem nsmul_eq_zero_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
n x = 0 x = 0
theorem pow_eq_one_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : M} {n : } (hn : n 0) :
x ^ n = 1 x = 1
theorem nsmul_le_nsmul_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {m : } {n : } (ha : 0 < a) :
m a n a m n
theorem pow_le_pow_iff' {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} {m : } {n : } (ha : 1 < a) :
a ^ m a ^ n m n
theorem nsmul_lt_nsmul_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {m : } {n : } (ha : 0 < a) :
m a < n a m < n
theorem pow_lt_pow_iff' {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} {m : } {n : } (ha : 1 < a) :
a ^ m < a ^ n m < n
theorem Left.nsmul_neg_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) :
n x < 0 x < 0
theorem Left.pow_lt_one_iff' {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) :
x ^ n < 1 x < 1
theorem Left.pow_lt_one_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) :
x ^ n < 1 x < 1
theorem Right.nsmul_neg_iff {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) :
n x < 0 x < 0
theorem Right.pow_lt_one_iff {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : } {x : M} (hn : 0 < n) :
x ^ n < 1 x < 1
theorem zsmul_nonneg {G : Type u_1} [inst : SubNegMonoid G] [inst : Preorder G] [inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x x_1] {x : G} (H : 0 x) {n : } (hn : 0 n) :
0 n x
theorem one_le_zpow {G : Type u_1} [inst : DivInvMonoid G] [inst : Preorder G] [inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x x_1] {x : G} (H : 1 x) {n : } (hn : 0 n) :
1 x ^ n
theorem CanonicallyOrderedCommSemiring.pow_pos {R : Type u_1} [inst : CanonicallyOrderedCommSemiring R] {a : R} (H : 0 < a) (n : ) :
0 < a ^ n
theorem zero_pow_le_one {R : Type u_1} [inst : OrderedSemiring R] (n : ) :
0 ^ n 1
theorem pow_add_pow_le {R : Type u_1} [inst : OrderedSemiring R] {x : R} {y : R} {n : } (hx : 0 x) (hy : 0 y) (hn : n 0) :
x ^ n + y ^ n (x + y) ^ n
theorem pow_le_one {R : Type u_1} [inst : OrderedSemiring R] {a : R} (n : ) :
0 aa 1a ^ n 1
theorem pow_lt_one {R : Type u_1} [inst : OrderedSemiring R] {a : R} (h₀ : 0 a) (h₁ : a < 1) {n : } :
n 0a ^ n < 1
theorem one_le_pow_of_one_le {R : Type u_1} [inst : OrderedSemiring R] {a : R} (H : 1 a) (n : ) :
1 a ^ n
theorem pow_mono {R : Type u_1} [inst : OrderedSemiring R] {a : R} (h : 1 a) :
Monotone fun n => a ^ n
theorem pow_le_pow {R : Type u_1} [inst : OrderedSemiring R] {a : R} {n : } {m : } (ha : 1 a) (h : n m) :
a ^ n a ^ m
theorem le_self_pow {R : Type u_1} [inst : OrderedSemiring R] {a : R} {m : } (ha : 1 a) (h : m 0) :
a a ^ m
theorem pow_le_pow_of_le_left {R : Type u_1} [inst : OrderedSemiring R] {a : R} {b : R} (ha : 0 a) (hab : a b) (i : ) :
a ^ i b ^ i
theorem one_lt_pow {R : Type u_1} [inst : OrderedSemiring R] {a : R} (ha : 1 < a) {n : } :
n 01 < a ^ n
theorem pow_lt_pow_of_lt_left {R : Type u_1} [inst : StrictOrderedSemiring R] {x : R} {y : R} (h : x < y) (hx : 0 x) {n : } :
0 < nx ^ n < y ^ n
theorem strictMonoOn_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {n : } (hn : 0 < n) :
StrictMonoOn (fun x => x ^ n) (Set.Ici 0)
theorem strictMono_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (h : 1 < a) :
StrictMono fun n => a ^ n
theorem pow_lt_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} {n : } {m : } (h : 1 < a) (h2 : n < m) :
a ^ n < a ^ m
theorem pow_lt_pow_iff {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} {n : } {m : } (h : 1 < a) :
a ^ n < a ^ m n < m
theorem pow_le_pow_iff {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} {n : } {m : } (h : 1 < a) :
a ^ n a ^ m n m
theorem strictAnti_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (h₀ : 0 < a) (h₁ : a < 1) :
StrictAnti fun n => a ^ n
theorem pow_lt_pow_iff_of_lt_one {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} {n : } {m : } (h₀ : 0 < a) (h₁ : a < 1) :
a ^ m < a ^ n n < m
theorem pow_lt_pow_of_lt_one {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (h : 0 < a) (ha : a < 1) {i : } {j : } (hij : i < j) :
a ^ j < a ^ i
theorem pow_lt_self_of_lt_one {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} {n : } (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) :
a ^ n < a
theorem sq_pos_of_pos {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (ha : 0 < a) :
0 < a ^ 2
theorem pow_bit0_pos_of_neg {R : Type u_1} [inst : StrictOrderedRing R] {a : R} (ha : a < 0) (n : ) :
0 < a ^ bit0 n
theorem pow_bit1_neg {R : Type u_1} [inst : StrictOrderedRing R] {a : R} (ha : a < 0) (n : ) :
a ^ bit1 n < 0
theorem sq_pos_of_neg {R : Type u_1} [inst : StrictOrderedRing R] {a : R} (ha : a < 0) :
0 < a ^ 2
theorem pow_le_one_iff_of_nonneg {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) {n : } (hn : n 0) :
a ^ n 1 a 1
theorem one_le_pow_iff_of_nonneg {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) {n : } (hn : n 0) :
1 a ^ n 1 a
theorem one_lt_pow_iff_of_nonneg {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) {n : } (hn : n 0) :
1 < a ^ n 1 < a
theorem pow_lt_one_iff_of_nonneg {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) {n : } (hn : n 0) :
a ^ n < 1 a < 1
theorem sq_le_one_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) :
a ^ 2 1 a 1
theorem sq_lt_one_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) :
a ^ 2 < 1 a < 1
theorem one_le_sq_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) :
1 a ^ 2 1 a
theorem one_lt_sq_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 a) :
1 < a ^ 2 1 < a
@[simp]
theorem pow_left_inj {R : Type u_1} [inst : LinearOrderedSemiring R] {x : R} {y : R} {n : } (Hxpos : 0 x) (Hypos : 0 y) (Hnpos : 0 < n) :
x ^ n = y ^ n x = y
theorem lt_of_pow_lt_pow {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} {b : R} (n : ) (hb : 0 b) (h : a ^ n < b ^ n) :
a < b
theorem le_of_pow_le_pow {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} {b : R} (n : ) (hb : 0 b) (hn : 0 < n) (h : a ^ n b ^ n) :
a b
@[simp]
theorem sq_eq_sq {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} {b : R} (ha : 0 a) (hb : 0 b) :
a ^ 2 = b ^ 2 a = b
theorem lt_of_mul_self_lt_mul_self {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} {b : R} (hb : 0 b) :
a * a < b * ba < b
theorem pow_abs {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (n : ) :
abs a ^ n = abs (a ^ n)
theorem abs_neg_one_pow {R : Type u_1} [inst : LinearOrderedRing R] (n : ) :
abs ((-1) ^ n) = 1
theorem pow_bit0_nonneg {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (n : ) :
0 a ^ bit0 n
theorem sq_nonneg {R : Type u_1} [inst : LinearOrderedRing R] (a : R) :
0 a ^ 2
theorem pow_two_nonneg {R : Type u_1} [inst : LinearOrderedRing R] (a : R) :
0 a ^ 2

Alias of sq_nonneg.

theorem pow_bit0_pos {R : Type u_1} [inst : LinearOrderedRing R] {a : R} (h : a 0) (n : ) :
0 < a ^ bit0 n
theorem sq_pos_of_ne_zero {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (h : a 0) :
0 < a ^ 2
theorem pow_two_pos_of_ne_zero {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (h : a 0) :
0 < a ^ 2

Alias of sq_pos_of_ne_zero.

theorem pow_bit0_pos_iff {R : Type u_1} [inst : LinearOrderedRing R] (a : R) {n : } (hn : n 0) :
0 < a ^ bit0 n a 0
theorem sq_pos_iff {R : Type u_1} [inst : LinearOrderedRing R] (a : R) :
0 < a ^ 2 a 0
theorem sq_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) :
abs x ^ 2 = x ^ 2
theorem abs_sq {R : Type u_1} [inst : LinearOrderedRing R] (x : R) :
abs (x ^ 2) = x ^ 2
theorem sq_lt_sq {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} :
x ^ 2 < y ^ 2 abs x < abs y
theorem sq_lt_sq' {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h1 : -y < x) (h2 : x < y) :
x ^ 2 < y ^ 2
theorem sq_le_sq {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} :
x ^ 2 y ^ 2 abs x abs y
theorem sq_le_sq' {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h1 : -y x) (h2 : x y) :
x ^ 2 y ^ 2
theorem abs_lt_of_sq_lt_sq {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 < y ^ 2) (hy : 0 y) :
abs x < y
theorem abs_lt_of_sq_lt_sq' {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 < y ^ 2) (hy : 0 y) :
-y < x x < y
theorem abs_le_of_sq_le_sq {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 y ^ 2) (hy : 0 y) :
abs x y
theorem abs_le_of_sq_le_sq' {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 y ^ 2) (hy : 0 y) :
-y x x y
theorem sq_eq_sq_iff_abs_eq_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) (y : R) :
x ^ 2 = y ^ 2 abs x = abs y
@[simp]
theorem sq_le_one_iff_abs_le_one {R : Type u_1} [inst : LinearOrderedRing R] (x : R) :
x ^ 2 1 abs x 1
@[simp]
theorem sq_lt_one_iff_abs_lt_one {R : Type u_1} [inst : LinearOrderedRing R] (x : R) :
x ^ 2 < 1 abs x < 1
@[simp]
theorem one_le_sq_iff_one_le_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) :
1 x ^ 2 1 abs x
@[simp]
theorem one_lt_sq_iff_one_lt_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) :
1 < x ^ 2 1 < abs x
theorem pow_four_le_pow_two_of_pow_two_le {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 y) :
x ^ 4 y ^ 2
theorem two_mul_le_add_sq {R : Type u_1} [inst : LinearOrderedCommRing R] (a : R) (b : R) :
2 * a * b a ^ 2 + b ^ 2

Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings.

theorem two_mul_le_add_pow_two {R : Type u_1} [inst : LinearOrderedCommRing R] (a : R) (b : R) :
2 * a * b a ^ 2 + b ^ 2

Alias of two_mul_le_add_sq.

theorem pow_pos_iff {M : Type u_1} [inst : LinearOrderedCommMonoidWithZero M] [inst : NoZeroDivisors M] {a : M} {n : } (hn : 0 < n) :
0 < a ^ n 0 < a
theorem pow_lt_pow_succ {M : Type u_1} [inst : LinearOrderedCommGroupWithZero M] {a : M} {n : } (ha : 1 < a) :
a ^ n < a ^ Nat.succ n
theorem pow_lt_pow₀ {M : Type u_1} [inst : LinearOrderedCommGroupWithZero M] {a : M} {m : } {n : } (ha : 1 < a) (hmn : m < n) :
a ^ m < a ^ n
theorem MonoidHom.map_neg_one {M : Type u_1} {R : Type u_2} [inst : Ring R] [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] (f : R →* M) :
f (-1) = 1
@[simp]
theorem MonoidHom.map_neg {M : Type u_1} {R : Type u_2} [inst : Ring R] [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] (f : R →* M) (x : R) :
f (-x) = f x
theorem MonoidHom.map_sub_swap {M : Type u_1} {R : Type u_2} [inst : Ring R] [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] (f : R →* M) (x : R) (y : R) :
f (x - y) = f (y - x)