# Documentation

Mathlib.Algebra.Ring.Units

# Units in semirings and rings #

instance Units.instNegUnits {α : Type u} [] [] :

Each element of the group of units of a ring has an additive inverse.

@[simp]
theorem Units.val_neg {α : Type u} [] [] (u : αˣ) :
↑(-u) = -u

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]
theorem Units.coe_neg_one {α : Type u} [] [] :
↑(-1) = -1
theorem Units.neg_divp {α : Type u} [] [] (a : α) (u : αˣ) :
-(a /ₚ u) = -a /ₚ u
theorem Units.divp_add_divp_same {α : Type u} [Ring α] (a : α) (b : α) (u : αˣ) :
a /ₚ u + b /ₚ u = (a + b) /ₚ u
theorem Units.divp_sub_divp_same {α : Type u} [Ring α] (a : α) (b : α) (u : αˣ) :
a /ₚ u - b /ₚ u = (a - b) /ₚ u
theorem Units.add_divp {α : Type u} [Ring α] (a : α) (b : α) (u : αˣ) :
a + b /ₚ u = (a * u + b) /ₚ u
theorem Units.sub_divp {α : Type u} [Ring α] (a : α) (b : α) (u : αˣ) :
a - b /ₚ u = (a * u - b) /ₚ u
theorem Units.divp_add {α : Type u} [Ring α] (a : α) (b : α) (u : αˣ) :
a /ₚ u + b = (a + b * u) /ₚ u
theorem Units.divp_sub {α : Type u} [Ring α] (a : α) (b : α) (u : αˣ) :
a /ₚ u - b = (a - b * u) /ₚ u
theorem IsUnit.neg {α : Type u} [] [] {a : α} :
IsUnit (-a)
@[simp]
theorem IsUnit.neg_iff {α : Type u} [] [] (a : α) :
theorem IsUnit.sub_iff {α : Type u} [Ring α] {x : α} {y : α} :
IsUnit (x - y) IsUnit (y - x)
theorem Units.divp_add_divp {α : Type u} [] (a : α) (b : α) (u₁ : αˣ) (u₂ : αˣ) :
a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂)
theorem Units.divp_sub_divp {α : Type u} [] (a : α) (b : α) (u₁ : αˣ) (u₂ : αˣ) :
a /ₚ u₁ - b /ₚ u₂ = (a * u₂ - u₁ * b) /ₚ (u₁ * u₂)
theorem Units.add_eq_mul_one_add_div {R : Type x} [] {a : Rˣ} {b : R} :
a + b = a * (1 + a⁻¹ * b)