Mathlib.Algebra.Order.Ring.Abs

mabs_zpow theorem

(n : ℤ) (a : α) : |a ^ n|ₘ = |a|ₘ ^ |n|

Full source

@[to_additive] lemma mabs_zpow (n : ℤ) (a : α) : |a ^ n|ₘ = |a|ₘ ^ |n| := by
  obtain n0 | n0 := le_total 0 n
  · obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
    simp only [mabs_pow, zpow_natCast, Nat.abs_cast]
  · obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
    rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]
    exact mabs_pow m _

Multiplicative Absolute Value of Integer Power: $|a^n|_m = |a|_m^{|n|}$

Informal description

For any integer $n$ and any element $a$ in a multiplicative lattice ordered group $\alpha$, the multiplicative absolute value of $a^n$ equals the multiplicative absolute value of $a$ raised to the absolute value of $n$, i.e., $|a^n|_m = |a|_m^{|n|}$.

odd_abs theorem

[LinearOrder α] [Ring α] {a : α} : Odd (abs a) ↔ Odd a

Full source

lemma odd_abs [LinearOrder α] [Ring α] {a : α} : OddOdd (abs a) ↔ Odd a := by
  rcases abs_choice a with h | h <;> simp only [h, odd_neg]

Oddness of Absolute Value in Linearly Ordered Rings

Informal description

Let $\alpha$ be a linearly ordered ring. For any element $a \in \alpha$, the absolute value $|a|$ is odd if and only if $a$ itself is odd.

abs_one theorem

: |(1 : α)| = 1

Full source

@[simp] lemma abs_one : |(1 : α)| = 1 := abs_of_pos zero_lt_one

Absolute Value of One: $|1| = 1$

Informal description

In any linearly ordered ring $\alpha$, the absolute value of the multiplicative identity $1$ is equal to $1$, i.e., $|1| = 1$.

abs_two theorem

: |(2 : α)| = 2

Full source

lemma abs_two : |(2 : α)| = 2 := abs_of_pos zero_lt_two

Absolute Value of Two: $|2| = 2$

Informal description

In any linearly ordered ring $\alpha$, the absolute value of the element $2$ is equal to $2$, i.e., $|2| = 2$.

abs_mul theorem

(a b : α) : |a * b| = |a| * |b|

Full source

lemma abs_mul (a b : α) : |a * b| = |a| * |b| := by
  rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
  rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
    simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, eq_self_iff_true, neg_mul,
      mul_neg, neg_neg, *]

Absolute Value Multiplicative Property: $|a \cdot b| = |a| \cdot |b|$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$, the absolute value of their product equals the product of their absolute values, i.e., $|a \cdot b| = |a| \cdot |b|$.

absHom definition

: α →*₀ α

Full source

/-- `abs` as a `MonoidWithZeroHom`. -/
def absHom : α →*₀ α where
  toFun := abs
  map_zero' := abs_zero
  map_one' := abs_one
  map_mul' := abs_mul

Absolute value as a monoid homomorphism with zero

Informal description

The absolute value function viewed as a monoid homomorphism with zero, i.e., a map $|\cdot| : \alpha \to \alpha$ that preserves multiplication, zero, and one, satisfying $|0| = 0$, $|1| = 1$, and $|a \cdot b| = |a| \cdot |b|$ for all $a, b \in \alpha$.

abs_pow theorem

(a : α) (n : ℕ) : |a ^ n| = |a| ^ n

Full source

@[simp]
lemma abs_pow (a : α) (n : ℕ) : |a ^ n| = |a| ^ n := (absHom.toMonoidHom : α →* α).map_pow _ _

Absolute Value Power Identity: $|a^n| = |a|^n$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any natural number $n$, the absolute value of $a^n$ equals the $n$-th power of the absolute value of $a$, i.e., $|a^n| = |a|^n$.

pow_abs theorem

(a : α) (n : ℕ) : |a| ^ n = |a ^ n|

Full source

lemma pow_abs (a : α) (n : ℕ) : |a| ^ n = |a ^ n| := (abs_pow a n).symm

Power of Absolute Value Equals Absolute Value of Power: $|a|^n = |a^n|$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any natural number $n$, the $n$-th power of the absolute value of $a$ equals the absolute value of $a^n$, i.e., $|a|^n = |a^n|$.

Even.pow_abs theorem

(hn : Even n) (a : α) : |a| ^ n = a ^ n

Full source

lemma Even.pow_abs (hn : Even n) (a : α) : |a| ^ n = a ^ n := by
  rw [← abs_pow, abs_eq_self]; exact hn.pow_nonneg _

Absolute Value Power Identity for Even Exponents: $|a|^n = a^n$ when $n$ is even

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any even natural number $n$, the $n$-th power of the absolute value of $a$ equals the $n$-th power of $a$, i.e., $|a|^n = a^n$.

abs_neg_one_pow theorem

(n : ℕ) : |(-1 : α) ^ n| = 1

Full source

lemma abs_neg_one_pow (n : ℕ) : |(-1 : α) ^ n| = 1 := by rw [← pow_abs, abs_neg, abs_one, one_pow]

Absolute Value of Negative One to a Natural Power: $|(-1)^n| = 1$

Informal description

For any natural number $n$, the absolute value of $(-1)^n$ in a linearly ordered ring $\alpha$ is equal to $1$, i.e., $|(-1)^n| = 1$.

abs_pow_eq_one theorem

(a : α) (h : n ≠ 0) : |a ^ n| = 1 ↔ |a| = 1

Full source

lemma abs_pow_eq_one (a : α) (h : n ≠ 0) : |a ^ n||a ^ n| = 1 ↔ |a| = 1 := by
  convert pow_left_inj₀ (abs_nonneg a) zero_le_one h
  exacts [(pow_abs _ _).symm, (one_pow _).symm]

Absolute Value Power Condition: $|a^n| = 1 \leftrightarrow |a| = 1$ for $n \neq 0$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any nonzero natural number $n$, the absolute value of $a^n$ equals $1$ if and only if the absolute value of $a$ equals $1$, i.e., $|a^n| = 1 \leftrightarrow |a| = 1$.

abs_mul_abs_self theorem

(a : α) : |a| * |a| = a * a

Full source

@[simp] lemma abs_mul_abs_self (a : α) : |a| * |a| = a * a :=
  abs_by_cases (fun x => x * x = a * a) rfl (neg_mul_neg a a)

Square of Absolute Value Equals Square of Element: $|a|^2 = a^2$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the product of the absolute value of $a$ with itself equals the square of $a$, i.e., $|a| \cdot |a| = a \cdot a$.

abs_mul_self theorem

(a : α) : |a * a| = a * a

Full source

@[simp]
lemma abs_mul_self (a : α) : |a * a| = a * a := by rw [abs_mul, abs_mul_abs_self]

Absolute Value of Square: $|a^2| = a^2$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the absolute value of the square of $a$ equals the square of $a$ itself, i.e., $|a \cdot a| = a \cdot a$.

abs_eq_iff_mul_self_eq theorem

: |a| = |b| ↔ a * a = b * b

Full source

lemma abs_eq_iff_mul_self_eq : |a||a| = |b| ↔ a * a = b * b := by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

Equality of Absolute Values via Squares: $|a| = |b| \leftrightarrow a^2 = b^2$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, the absolute values of $a$ and $b$ are equal if and only if their squares are equal, i.e., $|a| = |b| \leftrightarrow a^2 = b^2$.

abs_lt_iff_mul_self_lt theorem

: |a| < |b| ↔ a * a < b * b

Full source

lemma abs_lt_iff_mul_self_lt : |a||a| < |b| ↔ a * a < b * b := by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Absolute Value Inequality via Squares: $|a| < |b| \leftrightarrow a^2 < b^2$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, the absolute value of $a$ is less than the absolute value of $b$ if and only if the square of $a$ is less than the square of $b$, i.e., $|a| < |b| \leftrightarrow a^2 < b^2$.

abs_le_iff_mul_self_le theorem

: |a| ≤ |b| ↔ a * a ≤ b * b

Full source

lemma abs_le_iff_mul_self_le : |a||a| ≤ |b| ↔ a * a ≤ b * b := by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Absolute Value Comparison via Squares: $|a| \leq |b| \leftrightarrow a^2 \leq b^2$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, the absolute value of $a$ is less than or equal to the absolute value of $b$ if and only if the square of $a$ is less than or equal to the square of $b$, i.e., $|a| \leq |b| \leftrightarrow a^2 \leq b^2$.

abs_le_one_iff_mul_self_le_one theorem

: |a| ≤ 1 ↔ a * a ≤ 1

Full source

lemma abs_le_one_iff_mul_self_le_one : |a||a| ≤ 1 ↔ a * a ≤ 1 := by
  simpa only [abs_one, one_mul] using abs_le_iff_mul_self_le (a := a) (b := 1)

Absolute Value Bound via Squares: $|a| \leq 1 \leftrightarrow a^2 \leq 1$

Informal description

For any element $a$ in a linearly ordered ring, the absolute value of $a$ is less than or equal to $1$ if and only if the square of $a$ is less than or equal to $1$, i.e., $|a| \leq 1 \leftrightarrow a^2 \leq 1$.

sq_abs theorem

(a : α) : |a| ^ 2 = a ^ 2

Full source

@[simp] lemma sq_abs (a : α) : |a| ^ 2 = a ^ 2 := by simpa only [sq] using abs_mul_abs_self a

Square of Absolute Value Equals Square of Element: $|a|^2 = a^2$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the square of the absolute value of $a$ equals the square of $a$, i.e., $|a|^2 = a^2$.

abs_sq theorem

(x : α) : |x ^ 2| = x ^ 2

Full source

lemma abs_sq (x : α) : |x ^ 2| = x ^ 2 := by simpa only [sq] using abs_mul_self x

Absolute Value of Square: $|x^2| = x^2$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the absolute value of the square of $x$ equals the square of $x$ itself, i.e., $|x^2| = x^2$.

sq_lt_sq theorem

: a ^ 2 < b ^ 2 ↔ |a| < |b|

Full source

lemma sq_lt_sq : a ^ 2 < b ^ 2 ↔ |a| < |b| := by
  simpa only [sq_abs] using sq_lt_sq₀ (abs_nonneg a) (abs_nonneg b)

Square Inequality in Terms of Absolute Values: $a^2 < b^2 \leftrightarrow |a| < |b|$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, the inequality $a^2 < b^2$ holds if and only if the absolute value of $a$ is less than the absolute value of $b$, i.e., $a^2 < b^2 \leftrightarrow |a| < |b|$.

sq_lt_sq' theorem

(h1 : -b < a) (h2 : a < b) : a ^ 2 < b ^ 2

Full source

lemma sq_lt_sq' (h1 : -b < a) (h2 : a < b) : a ^ 2 < b ^ 2 :=
  sq_lt_sq.2 (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _))

Square Inequality under Boundedness: $a^2 < b^2$ when $-b < a < b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $-b < a$ and $a < b$, then $a^2 < b^2$.

sq_le_sq theorem

: a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|

Full source

lemma sq_le_sq : a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b| := by
  simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b)

Square Inequality Equivalent to Absolute Value Inequality: $a^2 \leq b^2 \leftrightarrow |a| \leq |b|$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, the inequality $a^2 \leq b^2$ holds if and only if $|a| \leq |b|$.

sq_le_sq' theorem

(h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2

Full source

lemma sq_le_sq' (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 :=
  sq_le_sq.2 (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))

Square Inequality under Absolute Value Bounds: $a^2 \leq b^2$ when $-b \leq a \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $-b \leq a$ and $a \leq b$, then $a^2 \leq b^2$.

abs_lt_of_sq_lt_sq theorem

(h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : |a| < b

Full source

lemma abs_lt_of_sq_lt_sq (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : |a| < b := by
  rwa [← abs_of_nonneg hb, ← sq_lt_sq]

Absolute Value Bound from Square Inequality: $a^2 < b^2 \to |a| < b$ (for $b \geq 0$)

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $a^2 < b^2$ and $b$ is non-negative, then the absolute value of $a$ is less than $b$, i.e., $|a| < b$.

abs_lt_of_sq_lt_sq' theorem

(h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : -b < a ∧ a < b

Full source

lemma abs_lt_of_sq_lt_sq' (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : -b < a ∧ a < b :=
  abs_lt.1 <| abs_lt_of_sq_lt_sq h hb

Double Inequality from Square Inequality: $a^2 < b^2 \Rightarrow -b < a < b$ (for $b \geq 0$)

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $a^2 < b^2$ and $b$ is non-negative, then $a$ lies strictly between $-b$ and $b$, i.e., $-b < a < b$.

abs_le_of_sq_le_sq theorem

(h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : |a| ≤ b

Full source

lemma abs_le_of_sq_le_sq (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : |a| ≤ b := by
  rwa [← abs_of_nonneg hb, ← sq_le_sq]

Absolute Value Bound from Square Inequality: $a^2 \leq b^2 \Rightarrow |a| \leq b$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $a^2 \leq b^2$ and $b \geq 0$, then the absolute value of $a$ is less than or equal to $b$, i.e., $|a| \leq b$.

le_of_sq_le_sq theorem

(h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : a ≤ b

Full source

theorem le_of_sq_le_sq (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : a ≤ b :=
  le_abs_self a |>.trans <| abs_le_of_sq_le_sq h hb

Square Inequality Implies Order Relation: $a^2 \leq b^2 \Rightarrow a \leq b$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $a^2 \leq b^2$ and $b \geq 0$, then $a \leq b$.

abs_le_of_sq_le_sq' theorem

(h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : -b ≤ a ∧ a ≤ b

Full source

lemma abs_le_of_sq_le_sq' (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : -b ≤ a ∧ a ≤ b :=
  abs_le.1 <| abs_le_of_sq_le_sq h hb

Absolute Value Bounds from Square Inequality: $a^2 \leq b^2 \Rightarrow -b \leq a \leq b$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring, if $a^2 \leq b^2$ and $b \geq 0$, then $a$ lies in the interval $[-b, b]$, i.e., $-b \leq a \leq b$.

sq_eq_sq_iff_abs_eq_abs theorem

(a b : α) : a ^ 2 = b ^ 2 ↔ |a| = |b|

Full source

lemma sq_eq_sq_iff_abs_eq_abs (a b : α) : a ^ 2 = b ^ 2 ↔ |a| = |b| := by
  simp only [le_antisymm_iff, sq_le_sq]

Equality of Squares is Equivalent to Equality of Absolute Values

Informal description

For any two elements $a$ and $b$ in a linearly ordered ring, the squares of $a$ and $b$ are equal if and only if their absolute values are equal, i.e., $a^2 = b^2 \leftrightarrow |a| = |b|$.

sq_le_one_iff_abs_le_one theorem

(a : α) : a ^ 2 ≤ 1 ↔ |a| ≤ 1

Full source

@[simp] lemma sq_le_one_iff_abs_le_one (a : α) : a ^ 2 ≤ 1 ↔ |a| ≤ 1 := by
  simpa only [one_pow, abs_one] using sq_le_sq (a := a) (b := 1)

Square Inequality Equivalent to Absolute Value Inequality: $a^2 \leq 1 \leftrightarrow |a| \leq 1$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the inequality $a^2 \leq 1$ holds if and only if $|a| \leq 1$.

sq_lt_one_iff_abs_lt_one theorem

(a : α) : a ^ 2 < 1 ↔ |a| < 1

Full source

@[simp] lemma sq_lt_one_iff_abs_lt_one (a : α) : a ^ 2 < 1 ↔ |a| < 1 := by
  simpa only [one_pow, abs_one] using sq_lt_sq (a := a) (b := 1)

Square Less Than One iff Absolute Value Less Than One: $a^2 < 1 \leftrightarrow |a| < 1$

Informal description

For any element $a$ in a linearly ordered ring, the square of $a$ is less than $1$ if and only if the absolute value of $a$ is less than $1$, i.e., $a^2 < 1 \leftrightarrow |a| < 1$.

one_le_sq_iff_one_le_abs theorem

(a : α) : 1 ≤ a ^ 2 ↔ 1 ≤ |a|

Full source

@[simp] lemma one_le_sq_iff_one_le_abs (a : α) : 1 ≤ a ^ 2 ↔ 1 ≤ |a| := by
  simpa only [one_pow, abs_one] using sq_le_sq (a := 1) (b := a)

Square Inequality Equivalent to Absolute Value Inequality: $1 \leq a^2 \leftrightarrow 1 \leq |a|$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the inequality $1 \leq a^2$ holds if and only if $1 \leq |a|$.

one_lt_sq_iff_one_lt_abs theorem

(a : α) : 1 < a ^ 2 ↔ 1 < |a|

Full source

@[simp] lemma one_lt_sq_iff_one_lt_abs (a : α) : 1 < a ^ 2 ↔ 1 < |a| := by
  simpa only [one_pow, abs_one] using sq_lt_sq (a := 1) (b := a)

Square Inequality for Absolute Values: $1 < a^2 \leftrightarrow 1 < |a|$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the inequality $1 < a^2$ holds if and only if $1 < |a|$.

exists_abs_lt theorem

{α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : ∃ b > 0, |a| < b

Full source

lemma exists_abs_lt {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α]
    (a : α) : ∃ b > 0, |a| < b :=
  ⟨|a| + 1, lt_of_lt_of_le zero_lt_one <| by simp, lt_add_one |a|⟩

Existence of Positive Upper Bound for Absolute Value in Ordered Rings

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ with a strict order, there exists a positive element $b$ such that the absolute value of $a$ is less than $b$, i.e., $\exists b > 0, |a| < b$.

abs_sub_sq theorem

(a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

Full source

theorem abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b := by
  rw [abs_mul_abs_self]
  simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
    neg_add_rev, neg_neg, add_assoc]

Square of Absolute Difference: $|a - b|^2 = a^2 + b^2 - 2ab$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$, the square of the absolute value of their difference equals $a^2 + b^2 - 2ab$, i.e., $|a - b|^2 = a^2 + b^2 - 2ab$.

abs_unit_intCast theorem

(a : ℤˣ) : |((a : ℤ) : α)| = 1

Full source

lemma abs_unit_intCast (a : ℤℤˣ) : |((a : ℤ) : α)| = 1 := by
  cases Int.units_eq_one_or a <;> simp_all

Absolute Value of Integer Units in Ordered Rings: $|a| = 1$ for $a \in \mathbb{Z}^\times$

Informal description

For any unit $a$ in the integers (i.e., $a \in \mathbb{Z}^\times$), the absolute value of the image of $a$ in a linearly ordered ring $\alpha$ is equal to $1$, i.e., $|(a : \alpha)| = 1$.

abs_pow_sub_pow_le theorem

: |a ^ n - b ^ n| ≤ |a - b| * n * max |a| |b| ^ (n - 1)

Full source

theorem abs_pow_sub_pow_le : |a ^ n - b ^ n| ≤ |a - b| * n * max |a| |b| ^ (n - 1) := by
  obtain _ | n := n; · simp
  rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]
  exact mul_le_mul_of_nonneg_left (abs_geomSum_le ..) (abs_nonneg _)

Inequality for Difference of Powers: $|a^n - b^n| \leq |a - b| \cdot n \cdot \max(|a|, |b|)^{n-1}$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$ and any natural number $n$, the absolute value of the difference of their $n$-th powers satisfies the inequality: \[ |a^n - b^n| \leq |a - b| \cdot n \cdot \max(|a|, |b|)^{n-1}. \]

abs_dvd theorem

(a b : α) : |a| ∣ b ↔ a ∣ b

Full source

@[simp]
theorem abs_dvd (a b : α) : |a||a| ∣ b|a| ∣ b ↔ a ∣ b := by
  rcases abs_choice a with h | h <;> simp only [h, neg_dvd]

Absolute Value Divisibility: $|a| \mid b \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$, the absolute value of $a$ divides $b$ if and only if $a$ divides $b$. That is, $|a| \mid b \leftrightarrow a \mid b$.

abs_dvd_self theorem

(a : α) : |a| ∣ a

Full source

theorem abs_dvd_self (a : α) : |a||a| ∣ a :=
  (abs_dvd a a).mpr (dvd_refl a)

Absolute Value Divides Itself: $|a| \mid a$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the absolute value of $a$ divides $a$. That is, $|a| \mid a$.

dvd_abs theorem

(a b : α) : a ∣ |b| ↔ a ∣ b

Full source

@[simp]
theorem dvd_abs (a b : α) : a ∣ |b|a ∣ |b| ↔ a ∣ b := by
  rcases abs_choice b with h | h <;> simp only [h, dvd_neg]

Divisibility of Absolute Value in Linearly Ordered Rings

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$, the element $a$ divides the absolute value of $b$ if and only if $a$ divides $b$. That is, $a \mid |b| \leftrightarrow a \mid b$.

self_dvd_abs theorem

(a : α) : a ∣ |a|

Full source

theorem self_dvd_abs (a : α) : a ∣ |a| :=
  (dvd_abs a a).mpr (dvd_refl a)

Self-Divisibility of Absolute Value: $a \mid |a|$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the element $a$ divides its own absolute value, i.e., $a \mid |a|$.

abs_dvd_abs theorem

(a b : α) : |a| ∣ |b| ↔ a ∣ b

Full source

theorem abs_dvd_abs (a b : α) : |a||a| ∣ |b||a| ∣ |b| ↔ a ∣ b :=
  (abs_dvd _ _).trans (dvd_abs _ _)

Absolute Value Divisibility Equivalence: $|a| \mid |b| \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$, the absolute value of $a$ divides the absolute value of $b$ if and only if $a$ divides $b$. That is, $|a| \mid |b| \leftrightarrow a \mid b$.

pow_eq_pow_iff_of_ne_zero theorem

(hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Full source

lemma pow_eq_pow_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
  match n.even_xor_odd with
  | .inl hne => by simp only [*, and_true, ← abs_eq_abs,
    ← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]
  | .inr hn => by simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

Equality of Powers in Linear Ordered Rings: $a^n = b^n \leftrightarrow a = b \lor (a = -b \land \text{even } n)$ for $n \neq 0$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring and any nonzero natural number $n$, the equality $a^n = b^n$ holds if and only if either $a = b$ or $a = -b$ and $n$ is even.

pow_eq_pow_iff_cases theorem

: a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Full source

lemma pow_eq_pow_iff_cases : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n := by
  rcases eq_or_ne n 0 with rfl | hn <;> simp [pow_eq_pow_iff_of_ne_zero, *]

Equality of Powers in Linear Ordered Rings: $a^n = b^n \leftrightarrow n=0 \lor a=b \lor (a=-b \land \text{even } n)$

Informal description

For elements $a$ and $b$ in a linear ordered ring and a natural number $n$, the equality $a^n = b^n$ holds if and only if one of the following conditions is satisfied: 1. $n = 0$, or 2. $a = b$, or 3. $a = -b$ and $n$ is even.

pow_eq_one_iff_of_ne_zero theorem

(hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Full source

lemma pow_eq_one_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n := by
  simp [← pow_eq_pow_iff_of_ne_zero hn]

Solutions to $a^n = 1$ in Linearly Ordered Rings for $n \neq 0$

Informal description

For any element $a$ in a linearly ordered ring and any nonzero natural number $n$, the equation $a^n = 1$ holds if and only if either $a = 1$ or $a = -1$ and $n$ is even.

pow_eq_one_iff_cases theorem

: a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Full source

lemma pow_eq_one_iff_cases : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n := by
  simp [← pow_eq_pow_iff_cases]

Characterization of Solutions to $a^n = 1$ in Linearly Ordered Rings

Informal description

For any element $a$ in a linearly ordered ring and natural number $n$, the equation $a^n = 1$ holds if and only if either $n = 0$, or $a = 1$, or $a = -1$ and $n$ is even.

pow_eq_neg_pow_iff theorem

(hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Full source

lemma pow_eq_neg_pow_iff (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n :=
  match n.even_or_odd with
  | .inl he =>
    suffices a ^ n > -b ^ n by simpa [he, not_odd_iff_even.2 he] using this.ne'
    lt_of_lt_of_le (by simp [he.pow_pos hb]) (he.pow_nonneg _)
  | .inr ho => by
    simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]

Power Equality with Negative Power: $a^n = -b^n \leftrightarrow (a = -b \land \text{Odd}(n))$ for $b \neq 0$

Informal description

For any nonzero element $b$ in a linearly ordered ring, the equation $a^n = -b^n$ holds if and only if $a = -b$ and $n$ is odd.

pow_eq_neg_one_iff theorem

: a ^ n = -1 ↔ a = -1 ∧ Odd n

Full source

lemma pow_eq_neg_one_iff : a ^ n = -1 ↔ a = -1 ∧ Odd n := by
  simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero

Characterization of Solutions to $a^n = -1$ in Linearly Ordered Rings

Informal description

For any element $a$ in a linearly ordered ring and natural number $n$, the equation $a^n = -1$ holds if and only if $a = -1$ and $n$ is odd.

Odd.mod_even_iff theorem

(ha : Even a) : Odd (n % a) ↔ Odd n

Full source

/-- If `a` is even, then `n` is odd iff `n % a` is odd. -/
lemma Odd.mod_even_iff (ha : Even a) : OddOdd (n % a) ↔ Odd n :=
  ((even_sub' <| mod_le n a).mp <|
      even_iff_two_dvd.mpr <| (even_iff_two_dvd.mp ha).trans <| dvd_sub_mod n).symm

Oddness Preservation Under Modulo by Even Number: $\text{Odd}(n \bmod a) \leftrightarrow \text{Odd}(n)$ when $a$ is even

Informal description

For any even natural number $a$, the remainder $n \bmod a$ is odd if and only if $n$ is odd.

Even.mod_even_iff theorem

(ha : Even a) : Even (n % a) ↔ Even n

Full source

/-- If `a` is even, then `n` is even iff `n % a` is even. -/
lemma Even.mod_even_iff (ha : Even a) : EvenEven (n % a) ↔ Even n :=
  ((even_sub <| mod_le n a).mp <|
      even_iff_two_dvd.mpr <| (even_iff_two_dvd.mp ha).trans <| dvd_sub_mod n).symm

Even Remainder Modulo Even Divisor: $\text{Even}(n \bmod a) \leftrightarrow \text{Even}(n)$ when $a$ is even

Informal description

For any even natural number $a$, the remainder $n \bmod a$ is even if and only if $n$ is even.

Odd.mod_even theorem

(hn : Odd n) (ha : Even a) : Odd (n % a)

Full source

/-- If `n` is odd and `a` is even, then `n % a` is odd. -/
lemma Odd.mod_even (hn : Odd n) (ha : Even a) : Odd (n % a) := (Odd.mod_even_iff ha).mpr hn

Odd Remainder of Odd Number Modulo Even Number

Informal description

For any natural numbers $n$ and $a$, if $n$ is odd and $a$ is even, then the remainder $n \bmod a$ is odd.

Even.mod_even theorem

(hn : Even n) (ha : Even a) : Even (n % a)

Full source

/-- If `n` is even and `a` is even, then `n % a` is even. -/
lemma Even.mod_even (hn : Even n) (ha : Even a) : Even (n % a) :=
  (Even.mod_even_iff ha).mpr hn

Even Remainder of Even Number Modulo Even Divisor

Informal description

For any natural numbers $n$ and $a$, if both $n$ and $a$ are even, then the remainder $n \bmod a$ is also even.

Odd.of_dvd_nat theorem

(hn : Odd n) (hm : m ∣ n) : Odd m

Full source

lemma Odd.of_dvd_nat (hn : Odd n) (hm : m ∣ n) : Odd m :=
  not_even_iff_odd.1 <| mt hm.even (not_even_iff_odd.2 hn)

Odd Divisors of Odd Numbers are Odd

Informal description

For any natural numbers $m$ and $n$, if $n$ is odd and $m$ divides $n$, then $m$ is also odd.

Odd.ne_two_of_dvd_nat theorem

{m n : ℕ} (hn : Odd n) (hm : m ∣ n) : m ≠ 2

Full source

/-- `2` is not a factor of an odd natural number. -/
lemma Odd.ne_two_of_dvd_nat {m n : ℕ} (hn : Odd n) (hm : m ∣ n) : m ≠ 2 := by
  rintro rfl
  exact absurd (hn.of_dvd_nat hm) (by decide)

Odd Numbers Have No Even Divisor Equal to Two

Informal description

For any natural numbers $m$ and $n$, if $n$ is odd and $m$ divides $n$, then $m$ is not equal to $2$.