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.

ink

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

ink

abbrev nsmul_le_nsmul_of_le_right.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive (Nat.succ k)) → motive x

Equations

• nsmul_le_nsmul_of_le_right.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

• nsmul_le_nsmul.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem CanonicallyOrderedCommSemiring.pow_pos {R : Type u_1} [inst : CanonicallyOrderedCommSemiring R] {a : R} (H : 0 < a) (n : ℕ) : 0 < a ^ n

ink

theorem zero_pow_le_one {R : Type u_1} [inst : OrderedSemiring R] (n : ℕ) : 0 ^ n ≤ 1

ink

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

ink

theorem pow_le_one {R : Type u_1} [inst : OrderedSemiring R] {a : R} (n : ℕ) : 0 ≤ a → a ≤ 1 → a ^ n ≤ 1

ink

theorem pow_lt_one {R : Type u_1} [inst : OrderedSemiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} : n ≠ 0 → a ^ n < 1

ink

theorem one_le_pow_of_one_le {R : Type u_1} [inst : OrderedSemiring R] {a : R} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n

ink

theorem pow_mono {R : Type u_1} [inst : OrderedSemiring R] {a : R} (h : 1 ≤ a) : Monotone fun n => a ^ n

ink

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

ink

theorem le_self_pow {R : Type u_1} [inst : OrderedSemiring R] {a : R} {m : ℕ} (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m

ink

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

ink

theorem one_lt_pow {R : Type u_1} [inst : OrderedSemiring R] {a : R} (ha : 1 < a) {n : ℕ} : n ≠ 0 → 1 < a ^ n

ink

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 < n → x ^ n < y ^ n

ink

theorem strictMonoOn_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {n : ℕ} (hn : 0 < n) : StrictMonoOn (fun x => x ^ n) (Set.Ici 0)

ink

theorem strictMono_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (h : 1 < a) : StrictMono fun n => a ^ n

ink

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

ink

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

ink

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

ink

theorem strictAnti_pow {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun n => a ^ n

ink

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

ink

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

ink

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

ink

theorem sq_pos_of_pos {R : Type u_1} [inst : StrictOrderedSemiring R] {a : R} (ha : 0 < a) : 0 < a ^ 2

ink

theorem pow_bit0_pos_of_neg {R : Type u_1} [inst : StrictOrderedRing R] {a : R} (ha : a < 0) (n : ℕ) : 0 < a ^ bit0 n

ink

theorem pow_bit1_neg {R : Type u_1} [inst : StrictOrderedRing R] {a : R} (ha : a < 0) (n : ℕ) : a ^ bit1 n < 0

ink

theorem sq_pos_of_neg {R : Type u_1} [inst : StrictOrderedRing R] {a : R} (ha : a < 0) : 0 < a ^ 2

ink

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

ink

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

ink

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

ink

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

ink

theorem sq_le_one_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1

ink

theorem sq_lt_one_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1

ink

theorem one_le_sq_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a

ink

theorem one_lt_sq_iff {R : Type u_1} [inst : LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a

ink

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

ink

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

ink

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

ink

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

ink

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 * b → a < b

ink

theorem pow_abs {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (n : ℕ) : abs a ^ n = abs (a ^ n)

ink

theorem abs_neg_one_pow {R : Type u_1} [inst : LinearOrderedRing R] (n : ℕ) : abs ((-1) ^ n) = 1

ink

theorem pow_bit0_nonneg {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n

ink

theorem sq_nonneg {R : Type u_1} [inst : LinearOrderedRing R] (a : R) : 0 ≤ a ^ 2

ink

theorem pow_two_nonneg {R : Type u_1} [inst : LinearOrderedRing R] (a : R) : 0 ≤ a ^ 2

Alias of sq_nonneg.

ink

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

ink

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

ink

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.

ink

theorem pow_bit0_pos_iff {R : Type u_1} [inst : LinearOrderedRing R] (a : R) {n : ℕ} (hn : n ≠ 0) : 0 < a ^ bit0 n ↔ a ≠ 0

ink

theorem sq_pos_iff {R : Type u_1} [inst : LinearOrderedRing R] (a : R) : 0 < a ^ 2 ↔ a ≠ 0

ink

theorem sq_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) : abs x ^ 2 = x ^ 2

ink

theorem abs_sq {R : Type u_1} [inst : LinearOrderedRing R] (x : R) : abs (x ^ 2) = x ^ 2

ink

theorem sq_lt_sq {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} : x ^ 2 < y ^ 2 ↔ abs x < abs y

ink

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

ink

theorem sq_le_sq {R : Type u_1} [inst : LinearOrderedRing R] {x : R} {y : R} : x ^ 2 ≤ y ^ 2 ↔ abs x ≤ abs y

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

theorem sq_le_one_iff_abs_le_one {R : Type u_1} [inst : LinearOrderedRing R] (x : R) : x ^ 2 ≤ 1 ↔ abs x ≤ 1

ink

@[simp]

theorem sq_lt_one_iff_abs_lt_one {R : Type u_1} [inst : LinearOrderedRing R] (x : R) : x ^ 2 < 1 ↔ abs x < 1

ink

@[simp]

theorem one_le_sq_iff_one_le_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) : 1 ≤ x ^ 2 ↔ 1 ≤ abs x

ink

@[simp]

theorem one_lt_sq_iff_one_lt_abs {R : Type u_1} [inst : LinearOrderedRing R] (x : R) : 1 < x ^ 2 ↔ 1 < abs x

ink

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

ink

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.

ink

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.

ink

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

ink

theorem pow_lt_pow_succ {M : Type u_1} [inst : LinearOrderedCommGroupWithZero M] {a : M} {n : ℕ} (ha : 1 < a) : a ^ n < a ^ Nat.succ n

ink

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

ink

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

ink

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

ink

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)