mathlib3 documentation

algebra.order.ring.abs

Absolute values in linear ordered rings. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[simp]
theorem abs_one {α : Type u_1} [linear_ordered_ring α] :
|1| = 1
source
@[simp]
theorem abs_two {α : Type u_1} [linear_ordered_ring α] :
|2| = 2
source
theorem abs_mul {α : Type u_1} [linear_ordered_ring α] (a b : α) :
|a * b| = |a| * |b|
source
def abs_hom {α : Type u_1} [linear_ordered_ring α] :
α →*₀ α

abs as a monoid_with_zero_hom.

Equations
source
@[simp]
theorem abs_mul_abs_self {α : Type u_1} [linear_ordered_ring α] (a : α) :
|a| * |a| = a * a
source
@[simp]
theorem abs_mul_self {α : Type u_1} [linear_ordered_ring α] (a : α) :
|a * a| = a * a
source
@[simp]
theorem abs_eq_self {α : Type u_1} [linear_ordered_ring α] {a : α} :
|a| = a ↔ 0 ≤ a
source
@[simp]
theorem abs_eq_neg_self {α : Type u_1} [linear_ordered_ring α] {a : α} :
|a| = -a ↔ a ≤ 0
source
theorem abs_cases {α : Type u_1} [linear_ordered_ring α] (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

source
@[simp]
theorem max_zero_add_max_neg_zero_eq_abs_self {α : Type u_1} [linear_ordered_ring α] (a : α) :
linear_order.max a 0 + linear_order.max (-a) 0 = |a|
source
theorem abs_eq_iff_mul_self_eq {α : Type u_1} [linear_ordered_ring α] {a b : α} :
|a| = |b| ↔ a * a = b * b
source
theorem abs_lt_iff_mul_self_lt {α : Type u_1} [linear_ordered_ring α] {a b : α} :
|a| < |b| ↔ a * a < b * b
source
theorem abs_le_iff_mul_self_le {α : Type u_1} [linear_ordered_ring α] {a b : α} :
|a| ≤ |b| ↔ a * a ≤ b * b
source
theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} [linear_ordered_ring α] {a : α} :
|a| ≤ 1 ↔ a * a ≤ 1
source
theorem abs_sub_sq {α : Type u_1} [linear_ordered_comm_ring α] (a b : α) :
|a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
source
@[simp]
theorem abs_dvd {α : Type u_1} [ring α] [linear_order α] (a b : α) :
|a| ∣ b ↔ a ∣ b
source
theorem abs_dvd_self {α : Type u_1} [ring α] [linear_order α] (a : α) :
|a| ∣ a
source
@[simp]
theorem dvd_abs {α : Type u_1} [ring α] [linear_order α] (a b : α) :
a ∣ |b| ↔ a ∣ b
source
theorem self_dvd_abs {α : Type u_1} [ring α] [linear_order α] (a : α) :
a ∣ |a|
source
theorem abs_dvd_abs {α : Type u_1} [ring α] [linear_order α] (a b : α) :
|a| ∣ |b| ↔ a ∣ b