Absolute values in linear ordered rings.

theorem mabs_zpow {α : Type u_1} [LinearOrderedCommGroup α] (n : ℤ) (a : α) : mabs (a ^ n) = mabs a ^ |n|

theorem abs_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] (n : ℤ) (a : α) : |n • a| = |n| • |a|

theorem odd_abs {α : Type u_1} [LinearOrder α] [Ring α] {a : α} : Odd |a| ↔ Odd a

@[simp]

theorem abs_one {α : Type u_1} [LinearOrderedRing α] : |1| = 1

theorem abs_two {α : Type u_1} [LinearOrderedRing α] : |2| = 2

theorem abs_mul {α : Type u_1} [LinearOrderedRing α] (a b : α) : |a * b| = |a| * |b|

def absHom {α : Type u_1} [LinearOrderedRing α] : α →*₀ α

abs as a MonoidWithZeroHom.

Equations

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

@[simp]

theorem abs_pow {α : Type u_1} [LinearOrderedRing α] (a : α) (n : ℕ) : |a ^ n| = |a| ^ n

theorem pow_abs {α : Type u_1} [LinearOrderedRing α] (a : α) (n : ℕ) : |a| ^ n = |a ^ n|

theorem Even.pow_abs {α : Type u_1} [LinearOrderedRing α] {n : ℕ} (hn : Even n) (a : α) : |a| ^ n = a ^ n

theorem abs_neg_one_pow {α : Type u_1} [LinearOrderedRing α] (n : ℕ) : |(-1) ^ n| = 1

theorem abs_pow_eq_one {α : Type u_1} [LinearOrderedRing α] {n : ℕ} (a : α) (h : n ≠ 0) : |a ^ n| = 1 ↔ |a| = 1

@[simp]

theorem abs_mul_abs_self {α : Type u_1} [LinearOrderedRing α] (a : α) : |a| * |a| = a * a

@[simp]

theorem abs_mul_self {α : Type u_1} [LinearOrderedRing α] (a : α) : |a * a| = a * a

theorem abs_eq_iff_mul_self_eq {α : Type u_1} [LinearOrderedRing α] {a b : α} : |a| = |b| ↔ a * a = b * b

theorem abs_lt_iff_mul_self_lt {α : Type u_1} [LinearOrderedRing α] {a b : α} : |a| < |b| ↔ a * a < b * b

theorem abs_le_iff_mul_self_le {α : Type u_1} [LinearOrderedRing α] {a b : α} : |a| ≤ |b| ↔ a * a ≤ b * b

theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} [LinearOrderedRing α] {a : α} : |a| ≤ 1 ↔ a * a ≤ 1

@[simp]

theorem sq_abs {α : Type u_1} [LinearOrderedRing α] (a : α) : |a| ^ 2 = a ^ 2

theorem abs_sq {α : Type u_1} [LinearOrderedRing α] (x : α) : |x ^ 2| = x ^ 2

theorem sq_lt_sq {α : Type u_1} [LinearOrderedRing α] {a b : α} : a ^ 2 < b ^ 2 ↔ |a| < |b|

theorem sq_lt_sq' {α : Type u_1} [LinearOrderedRing α] {a b : α} (h1 : -b < a) (h2 : a < b) : a ^ 2 < b ^ 2

theorem sq_le_sq {α : Type u_1} [LinearOrderedRing α] {a b : α} : a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|

theorem sq_le_sq' {α : Type u_1} [LinearOrderedRing α] {a b : α} (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2

theorem abs_lt_of_sq_lt_sq {α : Type u_1} [LinearOrderedRing α] {a b : α} (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : |a| < b

theorem abs_lt_of_sq_lt_sq' {α : Type u_1} [LinearOrderedRing α] {a b : α} (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : -b < a ∧ a < b

theorem abs_le_of_sq_le_sq {α : Type u_1} [LinearOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : |a| ≤ b

theorem le_of_sq_le_sq {α : Type u_1} [LinearOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : a ≤ b

theorem abs_le_of_sq_le_sq' {α : Type u_1} [LinearOrderedRing α] {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} [LinearOrderedRing α] (a b : α) : a ^ 2 = b ^ 2 ↔ |a| = |b|

@[simp]

theorem sq_le_one_iff_abs_le_one {α : Type u_1} [LinearOrderedRing α] (a : α) : a ^ 2 ≤ 1 ↔ |a| ≤ 1

@[simp]

theorem sq_lt_one_iff_abs_lt_one {α : Type u_1} [LinearOrderedRing α] (a : α) : a ^ 2 < 1 ↔ |a| < 1

@[simp]

theorem one_le_sq_iff_one_le_abs {α : Type u_1} [LinearOrderedRing α] (a : α) : 1 ≤ a ^ 2 ↔ 1 ≤ |a|

@[simp]

theorem one_lt_sq_iff_one_lt_abs {α : Type u_1} [LinearOrderedRing α] (a : α) : 1 < a ^ 2 ↔ 1 < |a|

theorem exists_abs_lt {α : Type u_2} [LinearOrderedRing α] (a : α) : ∃ b > 0, |a| < b

theorem abs_sub_sq {α : Type u_1} [LinearOrderedCommRing α] (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

theorem abs_unit_intCast {α : Type u_1} [LinearOrderedCommRing α] (a : ℤˣ) : |↑↑a| = 1

theorem abs_pow_sub_pow_le {α : Type u_1} [LinearOrderedCommRing α] (a b : α) (n : ℕ) : |a ^ n - b ^ n| ≤ |a - b| * ↑n * (|a| ⊔ |b|) ^ (n - 1)

@[simp]

theorem abs_dvd {α : Type u_1} [Ring α] [LinearOrder α] (a b : α) : |a| ∣ b ↔ a ∣ b

theorem abs_dvd_self {α : Type u_1} [Ring α] [LinearOrder α] (a : α) : |a| ∣ a

@[simp]

theorem dvd_abs {α : Type u_1} [Ring α] [LinearOrder α] (a b : α) : a ∣ |b| ↔ a ∣ b

theorem self_dvd_abs {α : Type u_1} [Ring α] [LinearOrder α] (a : α) : a ∣ |a|

theorem abs_dvd_abs {α : Type u_1} [Ring α] [LinearOrder α] (a b : α) : |a| ∣ |b| ↔ a ∣ b

theorem pow_eq_pow_iff_of_ne_zero {R : Type u_2} [LinearOrderedRing R] {a 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} [LinearOrderedRing R] {a 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} [LinearOrderedRing R] {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} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

theorem pow_eq_neg_pow_iff {R : Type u_2} [LinearOrderedRing R] {a b : R} {n : ℕ} (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n

theorem pow_eq_neg_one_iff {R : Type u_2} [LinearOrderedRing R] {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.