Mathlib.Algebra.Group.Int.Units

Int.units_natAbs theorem

(u : ℤˣ) : natAbs u = 1

Full source

lemma units_natAbs (u : ℤℤˣ) : natAbs u = 1 :=
  Units.ext_iff.1 <|
    Nat.units_eq_one
      ⟨natAbs u, natAbs ↑u⁻¹, by rw [← natAbs_mul, Units.mul_inv]; rfl, by
        rw [← natAbs_mul, Units.inv_mul]; rfl⟩

Natural Absolute Value of Integer Units is One

Informal description

For any unit $u$ in the group of units of the integers $\mathbb{Z}^\times$, the natural absolute value of $u$ is equal to $1$, i.e., $\text{natAbs}(u) = 1$.

Int.natAbs_of_isUnit theorem

(hu : IsUnit u) : natAbs u = 1

Full source

@[simp] lemma natAbs_of_isUnit (hu : IsUnit u) : natAbs u = 1 := units_natAbs hu.unit

Natural Absolute Value of Integer Units is One

Informal description

For any integer $u$ that is a unit in the monoid $\mathbb{Z}$, the natural absolute value of $u$ is equal to $1$, i.e., $\text{natAbs}(u) = 1$.

Int.isUnit_eq_one_or theorem

(hu : IsUnit u) : u = 1 ∨ u = -1

Full source

lemma isUnit_eq_one_or (hu : IsUnit u) : u = 1 ∨ u = -1 := by
  simpa only [natAbs_of_isUnit hu] using natAbs_eq u

Characterization of Integer Units: $u = 1$ or $u = -1$

Informal description

For any integer $u$ that is a unit in the monoid $\mathbb{Z}$, either $u = 1$ or $u = -1$.

Int.isUnit_ne_iff_eq_neg theorem

(hu : IsUnit u) (hv : IsUnit v) : u ≠ v ↔ u = -v

Full source

lemma isUnit_ne_iff_eq_neg (hu : IsUnit u) (hv : IsUnit v) : u ≠ vu ≠ v ↔ u = -v := by
  obtain rfl | rfl := isUnit_eq_one_or hu <;> obtain rfl | rfl := isUnit_eq_one_or hv <;> decide

Integer Units are Equal or Negatives: $u \neq v \leftrightarrow u = -v$

Informal description

For any integers $u$ and $v$ that are units in the monoid $\mathbb{Z}$, we have $u \neq v$ if and only if $u = -v$.

Int.isUnit_eq_or_eq_neg theorem

(hu : IsUnit u) (hv : IsUnit v) : u = v ∨ u = -v

Full source

lemma isUnit_eq_or_eq_neg (hu : IsUnit u) (hv : IsUnit v) : u = v ∨ u = -v :=
  or_iff_not_imp_left.2 (isUnit_ne_iff_eq_neg hu hv).1

Integer Units are Equal or Negatives: $u = v$ or $u = -v$

Informal description

For any integers $u$ and $v$ that are units in the monoid $\mathbb{Z}$, either $u = v$ or $u = -v$.

Int.isUnit_iff theorem

: IsUnit u ↔ u = 1 ∨ u = -1

Full source

lemma isUnit_iff : IsUnitIsUnit u ↔ u = 1 ∨ u = -1 := by
  refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩
  rcases h with (rfl | rfl)
  · exact isUnit_one
  · exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

Characterization of Integer Units: $u = 1$ or $u = -1$

Informal description

An integer $u$ is a unit in the monoid $\mathbb{Z}$ if and only if $u = 1$ or $u = -1$.

Int.mul_eq_one_iff_eq_one_or_neg_one theorem

: u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Full source

lemma mul_eq_one_iff_eq_one_or_neg_one : u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1 := by
  refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
    obtain ⟨rfl, rfl⟩ := H <;> rfl

Product of Integers Equals One if and only if Both are One or Both are Negative One

Informal description

For any integers $u$ and $v$, the product $u \cdot v$ equals $1$ if and only if either both $u$ and $v$ are $1$, or both $u$ and $v$ are $-1$.

Int.mul_eq_neg_one_iff_eq_one_or_neg_one theorem

: u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Full source

lemma mul_eq_neg_one_iff_eq_one_or_neg_one : u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1 := by
  refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
    obtain ⟨rfl, rfl⟩ := H <;> rfl

Product Equals Negative One in Integers if and only if Factors are One and Negative One

Informal description

For any integers $u$ and $v$, the product $u \cdot v$ equals $-1$ if and only if either $u = 1$ and $v = -1$, or $u = -1$ and $v = 1$.

Int.isUnit_iff_natAbs_eq theorem

: IsUnit u ↔ u.natAbs = 1

Full source

lemma isUnit_iff_natAbs_eq : IsUnitIsUnit u ↔ u.natAbs = 1 := by simp [natAbs_eq_iff, isUnit_iff]

Characterization of Units in Integers via Absolute Value

Informal description

An integer $u$ is a unit in the multiplicative monoid of integers if and only if the absolute value of $u$ (as a natural number) equals 1, i.e., $|u| = 1$.

Int.ofNat_isUnit theorem

{n : ℕ} : IsUnit (n : ℤ) ↔ IsUnit n

Full source

@[norm_cast]
lemma ofNat_isUnit {n : ℕ} : IsUnitIsUnit (n : ℤ) ↔ IsUnit n := by simp [isUnit_iff_natAbs_eq]

Units in Natural Numbers and Integers via Coercion

Informal description

For any natural number $n$, the integer $n$ (viewed as an element of $\mathbb{Z}$) is a unit in the multiplicative monoid of integers if and only if $n$ is a unit in the multiplicative monoid of natural numbers.

Int.isUnit_mul_self theorem

(hu : IsUnit u) : u * u = 1

Full source

lemma isUnit_mul_self (hu : IsUnit u) : u * u = 1 :=
  (isUnit_eq_one_or hu).elim (fun h ↦ h.symm ▸ rfl) fun h ↦ h.symm ▸ rfl

Square of Integer Unit Equals One

Informal description

For any integer $u$ that is a unit in the multiplicative monoid of integers, the product of $u$ with itself equals $1$, i.e., $u \cdot u = 1$.

Int.isUnit_add_isUnit_eq_isUnit_add_isUnit theorem

 {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) (hd : IsUnit d) :
  a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Full source

lemma isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b)
    (hc : IsUnit c) (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c := by
  rw [isUnit_iff] at ha hb hc hd
  aesop

Sum of Integer Units Equals Sum of Integer Units if and only if Components are Equal or Swapped

Informal description

For any integers $a, b, c, d$ that are units in the multiplicative monoid of integers, the equality $a + b = c + d$ holds if and only if either ($a = c$ and $b = d$) or ($a = d$ and $b = c$).