# Absolute values in linear ordered rings. #

source
theorem mabs_zpow {α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] (n : ℤ) (a : α) :
|a ^ n|ₘ = |a|ₘ ^ |n|
source
theorem abs_zsmul {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (n : ℤ) (a : α) :
|n • a| = |n| • |a|
source
theorem odd_abs {α : Type u_1} [LinearOrder α] [Ring α] {a : α} :
Odd |a| ↔ Odd a
source
@[simp]
theorem abs_one {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] :
|1| = 1
source
theorem abs_two {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] :
|2| = 2
source
@[simp]
theorem abs_mul {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a b : α) :
|a * b| = |a| * |b|
source
def absHom {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] :
α →*₀ α

`abs` as a `MonoidWithZeroHom`.

Equations

- absHom = { toFun := abs, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem abs_pow {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a : α) (n : ℕ) :
|a ^ n| = |a| ^ n
source
theorem pow_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a : α) (n : ℕ) :
|a| ^ n = |a ^ n|
source
theorem Even.pow_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] {n : ℕ} (hn : Even n) (a : α) :
|a| ^ n = a ^ n
source
theorem abs_neg_one_pow {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (n : ℕ) :
|(-1) ^ n| = 1
source
@[simp]
theorem abs_mul_abs_self {α : Type u_1} [Ring α] [LinearOrder α] (a : α) :
|a| * |a| = a * a
source
theorem abs_mul_self {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a : α) :
|a * a| = a * a
source
@[simp]
theorem sq_abs {α : Type u_1} [Ring α] [LinearOrder α] (a : α) :
|a| ^ 2 = a ^ 2
source
theorem abs_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (x : α) :
|x ^ 2| = x ^ 2
source
theorem exists_abs_lt {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] [Nontrivial α] (a : α) :
∃ b > 0, |a| < b
source
theorem abs_pow_eq_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} (a : α) (h : n ≠ 0) :
|a ^ n| = 1 ↔ |a| = 1
source
theorem abs_eq_iff_mul_self_eq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
|a| = |b| ↔ a * a = b * b
source
theorem abs_lt_iff_mul_self_lt {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
|a| < |b| ↔ a * a < b * b
source
theorem abs_le_iff_mul_self_le {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
|a| ≤ |b| ↔ a * a ≤ b * b
source
theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} :
|a| ≤ 1 ↔ a * a ≤ 1
source
theorem sq_lt_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
a ^ 2 < b ^ 2 ↔ |a| < |b|
source
theorem sq_lt_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h1 : -b < a) (h2 : a < b) :
a ^ 2 < b ^ 2
source
theorem sq_le_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
source
theorem sq_le_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h1 : -b ≤ a) (h2 : a ≤ b) :
a ^ 2 ≤ b ^ 2
source
theorem abs_lt_of_sq_lt_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) :
|a| < b
source
theorem abs_lt_of_sq_lt_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) :
-b < a ∧ a < b
source
theorem abs_le_of_sq_le_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) :
|a| ≤ b
source
theorem le_of_sq_le_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) :
a ≤ b
source
theorem abs_le_of_sq_le_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) :
-b ≤ a ∧ a ≤ b
source
theorem sq_eq_sq_iff_abs_eq_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a b : α) :
a ^ 2 = b ^ 2 ↔ |a| = |b|
source
@[simp]
theorem sq_le_one_iff_abs_le_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
a ^ 2 ≤ 1 ↔ |a| ≤ 1
source
@[simp]
theorem sq_lt_one_iff_abs_lt_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
a ^ 2 < 1 ↔ |a| < 1
source
@[simp]
theorem one_le_sq_iff_one_le_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
1 ≤ a ^ 2 ↔ 1 ≤ |a|
source
@[simp]
theorem one_lt_sq_iff_one_lt_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
1 < a ^ 2 ↔ 1 < |a|
source
theorem abs_sub_sq {α : Type u_1} [CommRing α] [LinearOrder α] (a b : α) :
|a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
source
theorem abs_unit_intCast {α : Type u_1} [CommRing α] [LinearOrder α] [IsOrderedRing α] (a : ℤ ˣ) :
|↑↑a| = 1
source
theorem abs_pow_sub_pow_le {α : Type u_1} [CommRing α] [LinearOrder α] (a b : α) (n : ℕ) [IsOrderedRing α] :
|a ^ n - b ^ n| ≤ |a - b| * ↑n * max |a| |b| ^ (n - 1)
source
@[simp]
theorem abs_dvd {α : Type u_1} [Ring α] [LinearOrder α] (a b : α) :
|a| ∣ b ↔ a ∣ b
source
theorem abs_dvd_self {α : Type u_1} [Ring α] [LinearOrder α] (a : α) :
|a| ∣ a
source
@[simp]
theorem dvd_abs {α : Type u_1} [Ring α] [LinearOrder α] (a b : α) :
a ∣ |b| ↔ a ∣ b
source
theorem self_dvd_abs {α : Type u_1} [Ring α] [LinearOrder α] (a : α) :
a ∣ |a|
source
theorem abs_dvd_abs {α : Type u_1} [Ring α] [LinearOrder α] (a b : α) :
|a| ∣ |b| ↔ a ∣ b
source
theorem pow_eq_pow_iff_of_ne_zero {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n
source
theorem pow_eq_pow_iff_cases {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} :
a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
source
theorem pow_eq_one_iff_of_ne_zero {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} (hn : n ≠ 0) :
a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n
source
theorem pow_eq_one_iff_cases {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} :
a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
source
theorem pow_eq_neg_pow_iff {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} (hb : b ≠ 0) :
a ^ n = -b ^ n ↔ a = -b ∧ Odd n
source
theorem pow_eq_neg_one_iff {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} :
a ^ n = -1 ↔ a = -1 ∧ Odd n
source
theorem Odd.mod_even_iff {n a : ℕ} (ha : Even a) :
Odd (n % a) ↔ Odd n

If `a` is even, then `n` is odd iff `n % a` is odd.

source
theorem Even.mod_even_iff {n a : ℕ} (ha : Even a) :
Even (n % a) ↔ Even n

If `a` is even, then `n` is even iff `n % a` is even.

source
theorem Odd.mod_even {n a : ℕ} (hn : Odd n) (ha : Even a) :
Odd (n % a)

If `n` is odd and `a` is even, then `n % a` is odd.

source
theorem Even.mod_even {n a : ℕ} (hn : Even n) (ha : Even a) :
Even (n % a)

If `n` is even and `a` is even, then `n % a` is even.

source
theorem Odd.of_dvd_nat {m n : ℕ} (hn : Odd n) (hm : m ∣ n) :
Odd m
source
theorem Odd.ne_two_of_dvd_nat {m n : ℕ} (hn : Odd n) (hm : m ∣ n) :
m ≠ 2

`2` is not a factor of an odd natural number.