Basic lemmas about ordered rings #
theorem
IsSquare.nonneg
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsRightCancelAdd R]
[ZeroLEOneClass R]
[ExistsAddOfLE R]
[PosMulMono R]
[AddLeftStrictMono R]
{x : R}
(h : IsSquare x)
:
@[simp]
theorem
not_isSquare_of_neg
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsRightCancelAdd R]
[ZeroLEOneClass R]
[ExistsAddOfLE R]
[PosMulMono R]
[AddLeftStrictMono R]
{x : R}
(h : x < 0)
:
theorem
MonoidHom.map_neg_one
{M : Type u_2}
{R : Type u_3}
[Ring R]
[Monoid M]
[LinearOrder M]
[MulLeftMono M]
(f : R →* M)
:
@[simp]
theorem
MonoidHom.map_neg
{M : Type u_2}
{R : Type u_3}
[Ring R]
[Monoid M]
[LinearOrder M]
[MulLeftMono M]
(f : R →* M)
(x : R)
:
theorem
MonoidHom.map_sub_swap
{M : Type u_2}
{R : Type u_3}
[Ring R]
[Monoid M]
[LinearOrder M]
[MulLeftMono M]
(f : R →* M)
(x y : R)
:
theorem
sq_pos_of_neg
{R : Type u_3}
[Ring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{a : R}
(ha : a < 0)
:
A function f : α → R
is nonarchimedean if it satisfies the ultrametric inequality
f (a + b) ≤ max (f a) (f b)
for all a b : α
.
Equations
- IsNonarchimedean f = ∀ (a b : α), f (a + b) ≤ max (f a) (f b)
Instances For
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
add_sq_le
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a b : R}
[ExistsAddOfLE R]
:
theorem
add_pow_le
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a b : R}
[ExistsAddOfLE R]
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(n : ℕ)
:
theorem
Even.add_pow_le
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a b : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
:
theorem
Even.pow_nonneg
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
(a : R)
:
theorem
Even.pow_pos
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
(ha : a ≠ 0)
:
theorem
Even.pow_pos_iff
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Even n)
(h₀ : n ≠ 0)
:
theorem
Odd.pow_neg_iff
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_nonneg_iff
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_nonpos_iff
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_pos_iff
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
theorem
Odd.pow_nonpos
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing 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}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing 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}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
[ExistsAddOfLE R]
(hn : Odd n)
:
StrictMono fun (a : R) => a ^ n
theorem
Odd.pow_injective
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{n : ℕ}
(hn : Odd n)
:
Function.Injective fun (x : R) => x ^ n
theorem
Odd.pow_lt_pow
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{n : ℕ}
(hn : Odd n)
{a b : R}
:
theorem
Odd.pow_le_pow
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{n : ℕ}
(hn : Odd n)
{a b : R}
:
theorem
Odd.pow_inj
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{n : ℕ}
(hn : Odd n)
{a b : R}
:
theorem
sq_pos_iff
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{a : R}
:
theorem
sq_pos_of_ne_zero
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{a : R}
:
Alias of the reverse direction of sq_pos_iff
.
theorem
pow_two_pos_of_ne_zero
{R : Type u_3}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{a : R}
:
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}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a b : R}
[ExistsAddOfLE R]
(h : a ^ 2 ≤ b)
: