Absolute values in linear ordered rings.

@[simp]

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

@[simp]

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 = { toZeroHom := { toFun := abs, map_zero' := (_ : |0| = 0) }, map_one' := (_ : |1| = 1), map_mul' := (_ : ∀ (a b : α), |a * b| = |a| * |b|) }

@[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

@[simp]

theorem abs_eq_self {α : Type u_1} [LinearOrderedRing α] {a : α} : |a| = a ↔ 0 ≤ a

@[simp]

theorem abs_eq_neg_self {α : Type u_1} [LinearOrderedRing α] {a : α} : |a| = -a ↔ a ≤ 0

theorem abs_cases {α : Type u_1} [LinearOrderedRing α] (a : α) : |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

For an element a of a linear ordered ring, either abs a = a and 0 ≤ 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} [LinearOrderedRing α] (a : α) : max a 0 + max (-a) 0 = |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

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

@[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