# mathlib3documentation

algebra.ring.units

# Units in semirings and rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def units.has_neg {α : Type u} [monoid α]  :

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

Equations
@[protected, simp, norm_cast]
theorem units.coe_neg {α : Type u} [monoid α] (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.

@[protected, simp, norm_cast]
theorem units.coe_neg_one {α : Type u} [monoid α]  :
-1 = -1
@[protected, instance]
def units.has_distrib_neg {α : Type u} [monoid α]  :
Equations
theorem units.neg_divp {α : Type u} [monoid α] (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 is_unit.neg {α : Type u} [monoid α] {a : α} :
@[simp]
theorem is_unit.neg_iff {α : Type u} [monoid α] (a : α) :
theorem is_unit.sub_iff {α : Type u} [ring α] {x y : α} :
is_unit (x - y) is_unit (y - x)
theorem units.divp_add_divp {α : Type u} [comm_ring α] (a b : α) (u₁ u₂ : αˣ) :
a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂)
theorem units.divp_sub_divp {α : Type u} [comm_ring α] (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} [semiring R] {a : Rˣ} {b : R} :
a + b = a * (1 + a⁻¹ * b)