Documentation

Mathlib.Algebra.Order.Ring.Abs

Absolute values in linear ordered rings. #

@[simp]
theorem abs_one {α : Type u_1} [inst : LinearOrderedRing α] :
abs 1 = 1
@[simp]
theorem abs_two {α : Type u_1} [inst : LinearOrderedRing α] :
abs 2 = 2
theorem abs_mul {α : Type u_1} [inst : LinearOrderedRing α] (a : α) (b : α) :
abs (a * b) = abs a * abs b
def absHom {α : Type u_1} [inst : LinearOrderedRing α] :
α →*₀ α

abs as a MonoidWithZeroHom.

Equations
  • absHom = { toZeroHom := { toFun := abs, map_zero' := (_ : abs 0 = 0) }, map_one' := (_ : abs 1 = 1), map_mul' := (_ : ∀ (a b : α), abs (a * b) = abs a * abs b) }
@[simp]
theorem abs_mul_abs_self {α : Type u_1} [inst : LinearOrderedRing α] (a : α) :
abs a * abs a = a * a
@[simp]
theorem abs_mul_self {α : Type u_1} [inst : LinearOrderedRing α] (a : α) :
abs (a * a) = a * a
@[simp]
theorem abs_eq_self {α : Type u_1} [inst : LinearOrderedRing α] {a : α} :
abs a = a 0 a
@[simp]
theorem abs_eq_neg_self {α : Type u_1} [inst : LinearOrderedRing α] {a : α} :
abs a = -a a 0
theorem abs_cases {α : Type u_1} [inst : LinearOrderedRing α] (a : α) :
abs a = a 0 a abs a = -a a < 0

For an element a of a linear ordered ring, either abs a = a and 0 ≤ a≤ a, or abs a = -a and a < 0. Use cases on this lemma to automate linarith in inequalities

@[simp]
theorem max_zero_add_max_neg_zero_eq_abs_self {α : Type u_1} [inst : LinearOrderedRing α] (a : α) :
max a 0 + max (-a) 0 = abs a
theorem abs_eq_iff_mul_self_eq {α : Type u_1} [inst : LinearOrderedRing α] {a : α} {b : α} :
abs a = abs b a * a = b * b
theorem abs_lt_iff_mul_self_lt {α : Type u_1} [inst : LinearOrderedRing α] {a : α} {b : α} :
abs a < abs b a * a < b * b
theorem abs_le_iff_mul_self_le {α : Type u_1} [inst : LinearOrderedRing α] {a : α} {b : α} :
abs a abs b a * a b * b
theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} [inst : LinearOrderedRing α] {a : α} :
abs a 1 a * a 1
theorem abs_sub_sq {α : Type u_1} [inst : LinearOrderedCommRing α] (a : α) (b : α) :
abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b
@[simp]
theorem abs_dvd {α : Type u_1} [inst : Ring α] [inst : LinearOrder α] (a : α) (b : α) :
abs a b a b
theorem abs_dvd_self {α : Type u_1} [inst : Ring α] [inst : LinearOrder α] (a : α) :
abs a a
@[simp]
theorem dvd_abs {α : Type u_1} [inst : Ring α] [inst : LinearOrder α] (a : α) (b : α) :
a abs b a b
theorem self_dvd_abs {α : Type u_1} [inst : Ring α] [inst : LinearOrder α] (a : α) :
a abs a
theorem abs_dvd_abs {α : Type u_1} [inst : Ring α] [inst : LinearOrder α] (a : α) (b : α) :
abs a abs b a b