Documentation

Mathlib.Algebra.Order.Ring.Abs

Absolute values in linear ordered rings. #

source
theorem abs_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] (n : ℤ) (a : α) :
|n • a| = |n| • |a|
source
theorem mabs_zpow {α : Type u_1} [LinearOrderedCommGroup α] (n : ℤ) (a : α) :
mabs (a ^ n) = mabs a ^ |n|
source
@[simp]
theorem abs_one {α : Type u_1} [LinearOrderedRing α] :
|1| = 1
source
theorem abs_two {α : Type u_1} [LinearOrderedRing α] :
|2| = 2
source
theorem abs_mul {α : Type u_1} [LinearOrderedRing α] (a : α) (b : α) :
|a * b| = |a| * |b|
source
def absHom {α : Type u_1} [LinearOrderedRing α] :
α →*₀ α

abs as a MonoidWithZeroHom.

Equations
  • absHom = { toZeroHom := { toFun := abs, map_zero' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
    source
    @[simp]
    theorem abs_pow {α : Type u_1} [LinearOrderedRing α] (a : α) (n : ℕ) :
    |a ^ n| = |a| ^ n
    source
    theorem pow_abs {α : Type u_1} [LinearOrderedRing α] (a : α) (n : ℕ) :
    |a| ^ n = |a ^ n|
    source
    theorem abs_neg_one_pow {α : Type u_1} [LinearOrderedRing α] (n : ℕ) :
    |(-1) ^ n| = 1
    source
    theorem abs_pow_eq_one {α : Type u_1} [LinearOrderedRing α] {n : ℕ} (a : α) (h : n ≠ 0) :
    |a ^ n| = 1 ↔ |a| = 1
    source
    @[simp]
    theorem abs_mul_abs_self {α : Type u_1} [LinearOrderedRing α] (a : α) :
    |a| * |a| = a * a
    source
    @[simp]
    theorem abs_mul_self {α : Type u_1} [LinearOrderedRing α] (a : α) :
    |a * a| = a * a
    source
    theorem abs_eq_iff_mul_self_eq {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} :
    |a| = |b| ↔ a * a = b * b
    source
    theorem abs_lt_iff_mul_self_lt {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} :
    |a| < |b| ↔ a * a < b * b
    source
    theorem abs_le_iff_mul_self_le {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} :
    |a| ≤ |b| ↔ a * a ≤ b * b
    source
    theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} [LinearOrderedRing α] {a : α} :
    |a| ≤ 1 ↔ a * a ≤ 1
    source
    @[simp]
    theorem sq_abs {α : Type u_1} [LinearOrderedRing α] (a : α) :
    |a| ^ 2 = a ^ 2
    source
    theorem abs_sq {α : Type u_1} [LinearOrderedRing α] (x : α) :
    |x ^ 2| = x ^ 2
    source
    theorem sq_lt_sq {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} :
    a ^ 2 < b ^ 2 ↔ |a| < |b|
    source
    theorem sq_lt_sq' {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} (h1 : -b < a) (h2 : a < b) :
    a ^ 2 < b ^ 2
    source
    theorem sq_le_sq {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} :
    a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
    source
    theorem sq_le_sq' {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} (h1 : -b ≤ a) (h2 : a ≤ b) :
    a ^ 2 ≤ b ^ 2
    source
    theorem abs_lt_of_sq_lt_sq {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) :
    |a| < b
    source
    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
    source
    theorem abs_le_of_sq_le_sq {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) :
    |a| ≤ b
    source
    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
    source
    theorem sq_eq_sq_iff_abs_eq_abs {α : Type u_1} [LinearOrderedRing α] (a : α) (b : α) :
    a ^ 2 = b ^ 2 ↔ |a| = |b|
    source
    @[simp]
    theorem sq_le_one_iff_abs_le_one {α : Type u_1} [LinearOrderedRing α] (a : α) :
    a ^ 2 ≤ 1 ↔ |a| ≤ 1
    source
    @[simp]
    theorem sq_lt_one_iff_abs_lt_one {α : Type u_1} [LinearOrderedRing α] (a : α) :
    a ^ 2 < 1 ↔ |a| < 1
    source
    @[simp]
    theorem one_le_sq_iff_one_le_abs {α : Type u_1} [LinearOrderedRing α] (a : α) :
    1 ≤ a ^ 2 ↔ 1 ≤ |a|
    source
    @[simp]
    theorem one_lt_sq_iff_one_lt_abs {α : Type u_1} [LinearOrderedRing α] (a : α) :
    1 < a ^ 2 ↔ 1 < |a|
    source
    theorem exists_abs_lt {α : Type u_2} [LinearOrderedRing α] (a : α) :
    ∃ (b : α), b > 0 ∧ |a| < b
    source
    theorem abs_sub_sq {α : Type u_1} [LinearOrderedCommRing α] (a : α) (b : α) :
    |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
    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