Basic lemmas about ordered rings #
theorem
MonoidHom.map_neg_one
{M : Type u_2}
{R : Type u_3}
[Ring R]
[Monoid M]
[LinearOrder M]
[CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2]
(f : R →* M)
:
f (-1) = 1
@[simp]
theorem
MonoidHom.map_neg
{M : Type u_2}
{R : Type u_3}
[Ring R]
[Monoid M]
[LinearOrder M]
[CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2]
(f : R →* M)
(x : R)
:
theorem
MonoidHom.map_sub_swap
{M : Type u_2}
{R : Type u_3}
[Ring R]
[Monoid M]
[LinearOrder M]
[CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2]
(f : R →* M)
(x : R)
(y : R)
:
@[deprecated mul_le_one₀]
theorem
mul_le_one
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
{b : M₀}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(ha : a ≤ 1)
(hb₀ : 0 ≤ b)
(hb : b ≤ 1)
:
Alias of mul_le_one₀
.
@[deprecated pow_le_one₀]
theorem
pow_le_one
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
{n : ℕ}
:
Alias of pow_le_one₀
.
@[deprecated pow_lt_one₀]
theorem
pow_lt_one
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(h₀ : 0 ≤ a)
(h₁ : a < 1)
{n : ℕ}
:
Alias of pow_lt_one₀
.
@[deprecated one_le_pow₀]
theorem
one_le_pow_of_one_le
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(ha : 1 ≤ a)
{n : ℕ}
:
Alias of one_le_pow₀
.
@[deprecated one_lt_pow₀]
theorem
one_lt_pow
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(ha : 1 < a)
{n : ℕ}
:
Alias of one_lt_pow₀
.
@[deprecated pow_right_mono₀]
theorem
pow_right_mono
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(h : 1 ≤ a)
:
Alias of pow_right_mono₀
.
@[deprecated pow_le_pow_right₀]
theorem
pow_le_pow_right
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
{m : ℕ}
{n : ℕ}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(ha : 1 ≤ a)
(hmn : m ≤ n)
:
Alias of pow_le_pow_right₀
.
@[deprecated le_self_pow₀]
theorem
le_self_pow
{M₀ : Type u_1}
[MonoidWithZero M₀]
[Preorder M₀]
{a : M₀}
{n : ℕ}
[ZeroLEOneClass M₀]
[PosMulMono M₀]
[MulPosMono M₀]
(ha : 1 ≤ a)
(hn : n ≠ 0)
:
Alias of le_self_pow₀
.
theorem
Bound.le_self_pow_of_pos
{R : Type u_3}
[OrderedSemiring R]
{a : R}
{m : ℕ}
(ha : 1 ≤ a)
(h : 0 < m)
:
The bound
tactic can't handle m ≠ 0
goals yet, so we express as 0 < m
theorem
pow_le_pow_left
{R : Type u_3}
[OrderedSemiring R]
{a : R}
{b : R}
(ha : 0 ≤ a)
(hab : a ≤ b)
(n : ℕ)
:
@[reducible, inline]
abbrev
OrderedRing.toStrictOrderedRing
(α : Type u_4)
[OrderedRing α]
[NoZeroDivisors α]
[Nontrivial α]
:
Turn an ordered domain into a strict ordered ring.
Equations
Instances For
theorem
pow_left_strictMonoOn
{R : Type u_3}
[StrictOrderedSemiring R]
{n : ℕ}
(hn : n ≠ 0)
:
StrictMonoOn (fun (x : R) => x ^ n) {a : R | 0 ≤ a}
See also pow_left_strictMono
and Nat.pow_left_strictMono
.
theorem
pow_right_strictMono
{R : Type u_3}
[StrictOrderedSemiring R]
{a : R}
(h : 1 < a)
:
StrictMono fun (x : ℕ) => a ^ x
See also pow_right_strictMono'
.
theorem
lt_self_pow
{R : Type u_3}
[StrictOrderedSemiring R]
{a : R}
{m : ℕ}
(h : 1 < a)
(hm : 1 < m)
:
theorem
pow_right_strictAnti
{R : Type u_3}
[StrictOrderedSemiring R]
{a : R}
(h₀ : 0 < a)
(h₁ : a < 1)
:
StrictAnti fun (x : ℕ) => a ^ x
theorem
pow_lt_self_of_lt_one
{R : Type u_3}
[StrictOrderedSemiring R]
{a : R}
{n : ℕ}
(h₀ : 0 < a)
(h₁ : a < 1)
(hn : 1 < n)
:
theorem
pow_right_injective
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
(ha₀ : 0 < a)
(ha₁ : a ≠ 1)
:
Function.Injective fun (x : ℕ) => a ^ x
theorem
lt_of_pow_lt_pow_left
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{b : R}
(n : ℕ)
(hb : 0 ≤ b)
(h : a ^ n < b ^ n)
:
a < b
theorem
lt_of_mul_self_lt_mul_self
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{b : R}
(hb : 0 ≤ b)
:
Lemmas for canonically linear ordered semirings or linear ordered rings #
The slightly unusual typeclass assumptions [LinearOrderedSemiring R] [ExistsAddOfLE R]
cover two
more familiar settings:
[LinearOrderedRing R]
, egℤ
,ℚ
orℝ
[CanonicallyLinearOrderedSemiring R]
(although we don't actually have this typeclass), egℕ
,ℚ≥0
orℝ≥0
theorem
Even.pow_nonneg
{R : Type u_3}
[LinearOrderedSemiring R]
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
(a : R)
:
theorem
Even.pow_pos
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
(ha : a ≠ 0)
:
theorem
Even.pow_pos_iff
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
(h₀ : n ≠ 0)
:
theorem
Odd.pow_neg_iff
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_nonneg_iff
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_nonpos_iff
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_pos_iff
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_nonpos
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
Alias of the reverse direction of Odd.pow_nonpos_iff
.
theorem
Odd.pow_neg
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
Alias of the reverse direction of Odd.pow_neg_iff
.
theorem
Odd.strictMono_pow
{R : Type u_3}
[LinearOrderedSemiring R]
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
StrictMono fun (a : R) => a ^ n
Alias of the reverse direction of sq_pos_iff
.
Alias of the reverse direction of sq_pos_iff
.
Alias of the reverse direction of sq_pos_iff
.
theorem
pow_four_le_pow_two_of_pow_two_le
{R : Type u_3}
[LinearOrderedSemiring R]
{a : R}
{b : R}
[ExistsAddOfLE R]
(h : a ^ 2 ≤ b)
: