Mathlib.Algebra.Ring.Units

Units.instNeg instance

: Neg αˣ

Full source

/-- Each element of the group of units of a ring has an additive inverse. -/
instance : Neg αˣ :=
  ⟨fun u => ⟨-↑u, -↑u⁻¹, by simp, by simp⟩⟩

Negation Operation on Units of a Monoid

Informal description

For any monoid $\alpha$, the group of units $\alpha^\times$ has a negation operation that sends each unit $u$ to its additive inverse $-u$.

Units.val_neg theorem

(u : αˣ) : (↑(-u) : α) = -u

Full source

/-- Representing an element of a ring's unit group as an element of the ring commutes with
    mapping this element to its additive inverse. -/
@[simp, norm_cast]
protected theorem val_neg (u : αˣ) : (↑(-u) : α) = -u :=
  rfl

Negation Commutes with Unit Inclusion: $(-u) = -u$

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$, the canonical map from $\alpha^\times$ to $\alpha$ commutes with negation, i.e., $(-u) = -u$ where the first negation is in $\alpha^\times$ and the second is in $\alpha$.

Units.coe_neg_one theorem

: ((-1 : αˣ) : α) = -1

Full source

@[simp, norm_cast]
protected theorem coe_neg_one : ((-1 : αˣ) : α) = -1 :=
  rfl

Negation of Unit One in Group of Units

Informal description

The canonical map from the group of units $\alpha^\times$ to $\alpha$ maps the unit $-1$ to $-1$ in $\alpha$, i.e., $(-1 : \alpha^\times) = -1$ in $\alpha$.

Units.instHasDistribNeg instance

: HasDistribNeg αˣ

Full source

instance : HasDistribNeg αˣ :=
  Units.ext.hasDistribNeg _ Units.val_neg Units.val_mul

Distributive Negation on the Group of Units

Informal description

The group of units $\alpha^\times$ of a monoid $\alpha$ has a distributive negation operation, meaning that for any units $u, v \in \alpha^\times$, the negation satisfies $-(u \cdot v) = (-u) \cdot v = u \cdot (-v)$.

Units.neg_divp theorem

(a : α) (u : αˣ) : -(a /ₚ u) = -a /ₚ u

Full source

@[field_simps]
theorem neg_divp (a : α) (u : αˣ) : -(a /ₚ u) = -a /ₚ u := by simp only [divp, neg_mul]

Negation Distributes Over Division by a Unit: $-(a / u) = (-a) / u$

Informal description

For any element $a$ in a monoid $\alpha$ and any unit $u$ of $\alpha$, the negation of the division $a$ by $u$ equals the division of $-a$ by $u$, i.e., $-(a / u) = (-a) / u$.

Units.divp_add_divp_same theorem

(a b : α) (u : αˣ) : a /ₚ u + b /ₚ u = (a + b) /ₚ u

Full source

@[field_simps 1010]
theorem divp_add_divp_same (a b : α) (u : αˣ) : a /ₚ u + b /ₚ u = (a + b) /ₚ u := by
  simp only [divp, add_mul]

Additivity of Division by a Unit: $a /ₚ u + b /ₚ u = (a + b) /ₚ u$

Informal description

For any elements $a, b$ in a ring $\alpha$ and any unit $u \in \alpha^\times$, the sum of $a$ divided by $u$ and $b$ divided by $u$ equals the sum of $a$ and $b$ divided by $u$, i.e., $a /ₚ u + b /ₚ u = (a + b) /ₚ u$.

Units.divp_sub_divp_same theorem

(a b : α) (u : αˣ) : a /ₚ u - b /ₚ u = (a - b) /ₚ u

Full source

@[field_simps 1010]
theorem divp_sub_divp_same (a b : α) (u : αˣ) : a /ₚ u - b /ₚ u = (a - b) /ₚ u := by
  rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]

Subtractivity of Division by a Unit: $a /ₚ u - b /ₚ u = (a - b) /ₚ u$

Informal description

For any elements $a, b$ in a ring $\alpha$ and any unit $u \in \alpha^\times$, the difference of $a$ divided by $u$ and $b$ divided by $u$ equals the difference of $a$ and $b$ divided by $u$, i.e., $a /ₚ u - b /ₚ u = (a - b) /ₚ u$.

Units.add_divp theorem

(a b : α) (u : αˣ) : a + b /ₚ u = (a * u + b) /ₚ u

Full source

@[field_simps]
theorem add_divp (a b : α) (u : αˣ) : a + b /ₚ u = (a * u + b) /ₚ u := by
  simp only [divp, add_mul, Units.mul_inv_cancel_right]

Additive-Multiplicative Property for Division by a Unit: $a + b/u = (a u + b)/u$

Informal description

For any elements $a$ and $b$ in a ring $\alpha$ and any unit $u \in \alpha^\times$, the sum $a + b / u$ is equal to $(a \cdot u + b) / u$, where $/u$ denotes division by the unit $u$ (i.e., multiplication by $u^{-1}$).

Units.sub_divp theorem

(a b : α) (u : αˣ) : a - b /ₚ u = (a * u - b) /ₚ u

Full source

@[field_simps]
theorem sub_divp (a b : α) (u : αˣ) : a - b /ₚ u = (a * u - b) /ₚ u := by
  simp only [divp, sub_mul, Units.mul_inv_cancel_right]

Subtractive-Multiplicative Property for Division by a Unit: $a - b/u = (a u - b)/u$

Informal description

For any elements $a$ and $b$ in a ring $\alpha$ and any unit $u \in \alpha^\times$, the difference $a - b / u$ is equal to $(a \cdot u - b) / u$, where $/u$ denotes division by the unit $u$ (i.e., multiplication by $u^{-1}$).

Units.divp_add theorem

(a b : α) (u : αˣ) : a /ₚ u + b = (a + b * u) /ₚ u

Full source

@[field_simps]
theorem divp_add (a b : α) (u : αˣ) : a /ₚ u + b = (a + b * u) /ₚ u := by
  simp only [divp, add_mul, Units.mul_inv_cancel_right]

Additive Property for Division by a Unit: $(a / u) + b = (a + b u) / u$

Informal description

For any elements $a$ and $b$ in a ring $\alpha$ and any unit $u \in \alpha^\times$, the sum $(a / u) + b$ is equal to $(a + b \cdot u) / u$, where $/u$ denotes division by the unit $u$ (i.e., multiplication by $u^{-1}$).

Units.divp_sub theorem

(a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u

Full source

@[field_simps]
theorem divp_sub (a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u := by
  simp only [divp, sub_mul, sub_right_inj]
  rw [mul_assoc, Units.mul_inv, mul_one]

Subtraction Property for Division by a Unit: $(a / u) - b = (a - b u) / u$

Informal description

For any elements $a$ and $b$ in a ring $\alpha$ and any unit $u \in \alpha^\times$, the difference $(a / u) - b$ is equal to $(a - b \cdot u) / u$, where $/u$ denotes division by the unit $u$ (i.e., multiplication by $u^{-1}$).

Units.map_neg theorem

 {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) (u : αˣ) :
  map (f : α →* β) (-u) = -map (f : α →* β) u

Full source

@[simp]
protected theorem map_neg {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β]
    (f : F) (u : αˣ) : map (f : α →* β) (-u) = -map (f : α →* β) u :=
  ext (by simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg])

Negation Commutes with Induced Homomorphism on Units

Informal description

Let $\alpha$ and $\beta$ be rings, and let $F$ be a type with a `RingHomClass` instance from $\alpha$ to $\beta$. For any ring homomorphism $f \colon \alpha \to \beta$ and any unit $u \in \alpha^\times$, the image of $-u$ under the induced homomorphism on units equals the negation of the image of $u$, i.e., \[ \text{map}(f)(-u) = -\text{map}(f)(u). \]

Units.map_neg_one theorem

{F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) : map (f : α →* β) (-1) = -1

Full source

protected theorem map_neg_one {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β]
    (f : F) : map (f : α →* β) (-1) = -1 := by
  simp only [Units.map_neg, map_one]

Negation of Identity under Induced Homomorphism on Units

Informal description

Let $\alpha$ and $\beta$ be rings, and let $F$ be a type with a `RingHomClass` instance from $\alpha$ to $\beta$. For any ring homomorphism $f \colon \alpha \to \beta$, the image of $-1$ under the induced homomorphism on units equals $-1$, i.e., \[ \text{map}(f)(-1) = -1. \]

IsUnit.neg theorem

[Monoid α] [HasDistribNeg α] {a : α} : IsUnit a → IsUnit (-a)

Full source

theorem IsUnit.neg [Monoid α] [HasDistribNeg α] {a : α} : IsUnit a → IsUnit (-a)
  | ⟨x, hx⟩ => hx ▸ (-x).isUnit

Negation Preserves Invertibility in Monoids with Distributive Negation

Informal description

Let $\alpha$ be a monoid with a distributive negation operation. For any element $a \in \alpha$, if $a$ is a unit (i.e., invertible), then $-a$ is also a unit.

IsUnit.neg_iff theorem

[Monoid α] [HasDistribNeg α] (a : α) : IsUnit (-a) ↔ IsUnit a

Full source

@[simp]
theorem IsUnit.neg_iff [Monoid α] [HasDistribNeg α] (a : α) : IsUnitIsUnit (-a) ↔ IsUnit a :=
  ⟨fun h => neg_neg a ▸ h.neg, IsUnit.neg⟩

Negation Preserves Invertibility in Monoids with Distributive Negation

Informal description

Let $\alpha$ be a monoid with a distributive negation operation. For any element $a \in \alpha$, $-a$ is a unit if and only if $a$ is a unit.

isUnit_neg_one theorem

[Monoid α] [HasDistribNeg α] : IsUnit (-1 : α)

Full source

theorem isUnit_neg_one [Monoid α] [HasDistribNeg α] : IsUnit (-1 : α) := isUnit_one.neg

Negation of One is a Unit in Monoids with Distributive Negation

Informal description

Let $\alpha$ be a monoid equipped with a distributive negation operation. Then the element $-1$ is a unit (i.e., invertible) in $\alpha$.

IsUnit.sub_iff theorem

[Ring α] {x y : α} : IsUnit (x - y) ↔ IsUnit (y - x)

Full source

theorem IsUnit.sub_iff [Ring α] {x y : α} : IsUnitIsUnit (x - y) ↔ IsUnit (y - x) :=
  (IsUnit.neg_iff _).symm.trans <| neg_sub x y ▸ Iff.rfl

Invertibility of Differences in a Ring: $x - y$ is a unit $\iff$ $y - x$ is a unit

Informal description

Let $\alpha$ be a ring. For any elements $x, y \in \alpha$, the difference $x - y$ is a unit if and only if the difference $y - x$ is a unit.

Units.divp_add_divp theorem

[CommSemiring α] (a b : α) (u₁ u₂ : αˣ) : a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂)

Full source

@[field_simps]
theorem divp_add_divp [CommSemiring α] (a b : α) (u₁ u₂ : αˣ) :
    a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂) := by
  simp only [divp, add_mul, mul_inv_rev, val_mul]
  rw [mul_comm (↑u₁ * b), mul_comm b]
  rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]

Addition Formula for Division by Units in a Commutative Semiring: $a/u_1 + b/u_2 = (a u_2 + u_1 b)/(u_1 u_2)$

Informal description

Let $\alpha$ be a commutative semiring. For any elements $a, b \in \alpha$ and units $u_1, u_2 \in \alpha^\times$, the sum of $a$ divided by $u_1$ and $b$ divided by $u_2$ equals $(a \cdot u_2 + u_1 \cdot b)$ divided by $(u_1 \cdot u_2)$. In symbols: \[ a /ₚ u_1 + b /ₚ u_2 = (a \cdot u_2 + u_1 \cdot b) /ₚ (u_1 \cdot u_2). \]

Units.divp_sub_divp theorem

[CommRing α] (a b : α) (u₁ u₂ : αˣ) : a /ₚ u₁ - b /ₚ u₂ = (a * u₂ - u₁ * b) /ₚ (u₁ * u₂)

Full source

@[field_simps]
theorem divp_sub_divp [CommRing α] (a b : α) (u₁ u₂ : αˣ) :
    a /ₚ u₁ - b /ₚ u₂ = (a * u₂ - u₁ * b) /ₚ (u₁ * u₂) := by
  simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]

Subtraction Formula for Division by Units in a Commutative Ring: $a/u_1 - b/u_2 = (a u_2 - u_1 b)/(u_1 u_2)$

Informal description

Let $\alpha$ be a commutative ring. For any elements $a, b \in \alpha$ and units $u_1, u_2 \in \alpha^\times$, the difference of $a$ divided by $u_1$ and $b$ divided by $u_2$ equals $(a \cdot u_2 - u_1 \cdot b)$ divided by $(u_1 \cdot u_2)$. In symbols: \[ a /ₚ u_1 - b /ₚ u_2 = (a \cdot u_2 - u_1 \cdot b) /ₚ (u_1 \cdot u_2). \]

Units.add_eq_mul_one_add_div theorem

[Semiring R] {a : Rˣ} {b : R} : ↑a + b = a * (1 + ↑a⁻¹ * b)

Full source

theorem add_eq_mul_one_add_div [Semiring R] {a : Rˣ} {b : R} : ↑a + b = a * (1 + ↑a⁻¹ * b) := by
  rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]

Unit-Plus-Element Factorization in Semirings: $a + b = a(1 + a^{-1}b)$

Informal description

Let $R$ be a semiring, $a$ be a unit in $R$ (i.e., $a \in R^\times$), and $b$ be an element of $R$. Then the sum of $a$ (considered as an element of $R$) and $b$ can be expressed as: \[ a + b = a \cdot (1 + a^{-1} \cdot b) \] where $a^{-1}$ is the multiplicative inverse of $a$ in $R^\times$.

RingHom.isUnit_map theorem

(f : α →+* β) {a : α} : IsUnit a → IsUnit (f a)

Full source

theorem isUnit_map (f : α →+* β) {a : α} : IsUnit a → IsUnit (f a) :=
  IsUnit.map f

Ring Homomorphisms Preserve Units: $f(a) \in \beta^\times$ when $a \in \alpha^\times$

Informal description

Let $f \colon \alpha \to \beta$ be a ring homomorphism between semirings (or rings) $\alpha$ and $\beta$. For any element $a \in \alpha$ that is a unit (i.e., has a multiplicative inverse in $\alpha$), the image $f(a)$ is a unit in $\beta$.