# Absolute values in linear ordered rings. #

theorem abs_zsmul {α : Type u_1} (n : ) (a : α) :
|n a| = |n| |a|
theorem mabs_zpow {α : Type u_1} (n : ) (a : α) :
mabs (a ^ n) = mabs a ^ |n|
theorem odd_abs {α : Type u_1} [] [Ring α] {a : α} :
Odd |a| Odd a
@[simp]
theorem abs_one {α : Type u_1} :
|1| = 1
theorem abs_two {α : Type u_1} :
|2| = 2
theorem abs_mul {α : Type u_1} (a : α) (b : α) :
|a * b| = |a| * |b|
def absHom {α : Type u_1} :
α →*₀ α

abs as a MonoidWithZeroHom.

Equations
• absHom = { toFun := abs, map_zero' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem abs_pow {α : Type u_1} (a : α) (n : ) :
|a ^ n| = |a| ^ n
theorem pow_abs {α : Type u_1} (a : α) (n : ) :
|a| ^ n = |a ^ n|
theorem Even.pow_abs {α : Type u_1} {n : } (hn : Even n) (a : α) :
|a| ^ n = a ^ n
theorem abs_neg_one_pow {α : Type u_1} (n : ) :
|(-1) ^ n| = 1
theorem abs_pow_eq_one {α : Type u_1} {n : } (a : α) (h : n 0) :
|a ^ n| = 1 |a| = 1
@[simp]
theorem abs_mul_abs_self {α : Type u_1} (a : α) :
|a| * |a| = a * a
@[simp]
theorem abs_mul_self {α : Type u_1} (a : α) :
|a * a| = a * a
theorem abs_eq_iff_mul_self_eq {α : Type u_1} {a : α} {b : α} :
|a| = |b| a * a = b * b
theorem abs_lt_iff_mul_self_lt {α : Type u_1} {a : α} {b : α} :
|a| < |b| a * a < b * b
theorem abs_le_iff_mul_self_le {α : Type u_1} {a : α} {b : α} :
|a| |b| a * a b * b
theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} {a : α} :
|a| 1 a * a 1
@[simp]
theorem sq_abs {α : Type u_1} (a : α) :
|a| ^ 2 = a ^ 2
theorem abs_sq {α : Type u_1} (x : α) :
|x ^ 2| = x ^ 2
theorem sq_lt_sq {α : Type u_1} {a : α} {b : α} :
a ^ 2 < b ^ 2 |a| < |b|
theorem sq_lt_sq' {α : Type u_1} {a : α} {b : α} (h1 : -b < a) (h2 : a < b) :
a ^ 2 < b ^ 2
theorem sq_le_sq {α : Type u_1} {a : α} {b : α} :
a ^ 2 b ^ 2 |a| |b|
theorem sq_le_sq' {α : Type u_1} {a : α} {b : α} (h1 : -b a) (h2 : a b) :
a ^ 2 b ^ 2
theorem abs_lt_of_sq_lt_sq {α : Type u_1} {a : α} {b : α} (h : a ^ 2 < b ^ 2) (hb : 0 b) :
|a| < b
theorem abs_lt_of_sq_lt_sq' {α : Type u_1} {a : α} {b : α} (h : a ^ 2 < b ^ 2) (hb : 0 b) :
-b < a a < b
theorem abs_le_of_sq_le_sq {α : Type u_1} {a : α} {b : α} (h : a ^ 2 b ^ 2) (hb : 0 b) :
|a| b
theorem abs_le_of_sq_le_sq' {α : Type u_1} {a : α} {b : α} (h : a ^ 2 b ^ 2) (hb : 0 b) :
-b a a b
theorem sq_eq_sq_iff_abs_eq_abs {α : Type u_1} (a : α) (b : α) :
a ^ 2 = b ^ 2 |a| = |b|
@[simp]
theorem sq_le_one_iff_abs_le_one {α : Type u_1} (a : α) :
a ^ 2 1 |a| 1
@[simp]
theorem sq_lt_one_iff_abs_lt_one {α : Type u_1} (a : α) :
a ^ 2 < 1 |a| < 1
@[simp]
theorem one_le_sq_iff_one_le_abs {α : Type u_1} (a : α) :
1 a ^ 2 1 |a|
@[simp]
theorem one_lt_sq_iff_one_lt_abs {α : Type u_1} (a : α) :
1 < a ^ 2 1 < |a|
theorem exists_abs_lt {α : Type u_2} (a : α) :
b > 0, |a| < b
theorem abs_sub_sq {α : Type u_1} (a : α) (b : α) :
|a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
@[simp]
theorem abs_dvd {α : Type u_1} [Ring α] [] (a : α) (b : α) :
|a| b a b
theorem abs_dvd_self {α : Type u_1} [Ring α] [] (a : α) :
|a| a
@[simp]
theorem dvd_abs {α : Type u_1} [Ring α] [] (a : α) (b : α) :
a |b| a b
theorem self_dvd_abs {α : Type u_1} [Ring α] [] (a : α) :
a |a|
theorem abs_dvd_abs {α : Type u_1} [Ring α] [] (a : α) (b : α) :
|a| |b| a b
theorem pow_eq_pow_iff_of_ne_zero {R : Type u_2} {a : R} {b : R} {n : } (hn : n 0) :
a ^ n = b ^ n a = b a = -b Even n
theorem pow_eq_pow_iff_cases {R : Type u_2} {a : R} {b : R} {n : } :
a ^ n = b ^ n n = 0 a = b a = -b Even n
theorem pow_eq_one_iff_of_ne_zero {R : Type u_2} {a : R} {n : } (hn : n 0) :
a ^ n = 1 a = 1 a = -1 Even n
theorem pow_eq_one_iff_cases {R : Type u_2} {a : R} {n : } :
a ^ n = 1 n = 0 a = 1 a = -1 Even n
theorem pow_eq_neg_pow_iff {R : Type u_2} {a : R} {b : R} {n : } (hb : b 0) :
a ^ n = -b ^ n a = -b Odd n
theorem pow_eq_neg_one_iff {R : Type u_2} {a : R} {n : } :
a ^ n = -1 a = -1 Odd n
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.

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.

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.

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.

theorem Odd.of_dvd_nat {m : } {n : } (hn : Odd n) (hm : m n) :
Odd m
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.