Documentation

Mathlib.Algebra.Order.Ring.Abs

Absolute values in linear ordered rings. #

source
theorem mabs_zpow {α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] (n : ℤ) (a : α) :
|a ^ n|ₘ = |a|ₘ ^ |n|
source
theorem abs_zsmul {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (n : ℤ) (a : α) :
|n • a| = |n| • |a|
source
theorem odd_abs {α : Type u_1} [LinearOrder α] [Ring α] {a : α} :
Odd |a| ↔ Odd a
source
@[simp]
theorem abs_one {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] :
|1| = 1
source
theorem abs_two {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] :
|2| = 2
source
@[simp]
theorem abs_mul {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a b : α) :
|a * b| = |a| * |b|
source
def absHom {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] :
α →*₀ α

abs as a MonoidWithZeroHom.

Equations
  • absHom = { toFun := abs, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
    source
    @[simp]
    theorem abs_pow {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a : α) (n : ℕ) :
    |a ^ n| = |a| ^ n
    source
    theorem pow_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a : α) (n : ℕ) :
    |a| ^ n = |a ^ n|
    source
    theorem Even.pow_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] {n : ℕ} (hn : Even n) (a : α) :
    |a| ^ n = a ^ n
    source
    theorem abs_neg_one_pow {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (n : ℕ) :
    |(-1) ^ n| = 1
    source
    @[simp]
    theorem abs_mul_abs_self {α : Type u_1} [Ring α] [LinearOrder α] (a : α) :
    |a| * |a| = a * a
    source
    theorem abs_mul_self {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (a : α) :
    |a * a| = a * a
    source
    @[simp]
    theorem sq_abs {α : Type u_1} [Ring α] [LinearOrder α] (a : α) :
    |a| ^ 2 = a ^ 2
    source
    theorem abs_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] (x : α) :
    |x ^ 2| = x ^ 2
    source
    theorem exists_abs_lt {α : Type u_1} [Ring α] [LinearOrder α] [IsOrderedRing α] [Nontrivial α] (a : α) :
    ∃ (b : α), b > 0 ∧ |a| < b
    source
    theorem abs_pow_eq_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} (a : α) (h : n ≠ 0) :
    |a ^ n| = 1 ↔ |a| = 1
    source
    theorem abs_eq_iff_mul_self_eq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
    |a| = |b| ↔ a * a = b * b
    source
    theorem abs_lt_iff_mul_self_lt {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
    |a| < |b| ↔ a * a < b * b
    source
    theorem abs_le_iff_mul_self_le {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
    |a| ≤ |b| ↔ a * a ≤ b * b
    source
    theorem abs_le_one_iff_mul_self_le_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} :
    |a| ≤ 1 ↔ a * a ≤ 1
    source
    theorem sq_lt_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
    a ^ 2 < b ^ 2 ↔ |a| < |b|
    source
    theorem sq_lt_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h1 : -b < a) (h2 : a < b) :
    a ^ 2 < b ^ 2
    source
    theorem sq_le_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} :
    a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
    source
    theorem sq_le_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h1 : -b ≤ a) (h2 : a ≤ b) :
    a ^ 2 ≤ b ^ 2
    source
    theorem abs_lt_of_sq_lt_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) :
    |a| < b
    source
    theorem abs_lt_of_sq_lt_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) :
    |a| ≤ b
    source
    theorem le_of_sq_le_sq {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) :
    a ≤ b
    source
    theorem abs_le_of_sq_le_sq' {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a b : α) :
    a ^ 2 = b ^ 2 ↔ |a| = |b|
    source
    @[simp]
    theorem sq_le_one_iff_abs_le_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
    a ^ 2 ≤ 1 ↔ |a| ≤ 1
    source
    @[simp]
    theorem sq_lt_one_iff_abs_lt_one {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
    a ^ 2 < 1 ↔ |a| < 1
    source
    @[simp]
    theorem one_le_sq_iff_one_le_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
    1 ≤ a ^ 2 ↔ 1 ≤ |a|
    source
    @[simp]
    theorem one_lt_sq_iff_one_lt_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
    1 < a ^ 2 ↔ 1 < |a|
    source
    theorem abs_sub_sq {α : Type u_1} [CommRing α] [LinearOrder α] (a b : α) :
    |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
    source
    theorem abs_unit_intCast {α : Type u_1} [CommRing α] [LinearOrder α] [IsOrderedRing α] (a : ℤˣ) :
    |↑↑a| = 1
    source
    theorem abs_pow_sub_pow_le {α : Type u_1} [CommRing α] [LinearOrder α] (a b : α) (n : ℕ) [IsOrderedRing α] :
    |a ^ n - b ^ n| ≤ |a - b| * ↑n * max |a| |b| ^ (n - 1)
    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
    source
    theorem pow_eq_pow_iff_of_ne_zero {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} (hn : n ≠ 0) :
    a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n
    source
    theorem pow_eq_pow_iff_cases {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} :
    a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
    source
    theorem pow_eq_one_iff_of_ne_zero {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} (hn : n ≠ 0) :
    a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n
    source
    theorem pow_eq_one_iff_cases {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} :
    a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
    source
    theorem pow_eq_neg_pow_iff {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ} (hb : b ≠ 0) :
    a ^ n = -b ^ n ↔ a = -b ∧ Odd n
    source
    theorem pow_eq_neg_one_iff {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} :
    a ^ n = -1 ↔ a = -1 ∧ Odd n
    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    theorem Odd.of_dvd_nat {m n : ℕ} (hn : Odd n) (hm : m ∣ n) :
    Odd m
    source
    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.

    source
    theorem Int.le_abs_of_dvd {a b : ℤ} (h₁ : b ≠ 0) (h₂ : a ∣ b) :
    a ≤ |b|