Documentation

Mathlib.Algebra.Ring.Units

Units in semirings and rings #

instance Units.instNeg {α : Type u} [Monoid α] [HasDistribNeg α] :

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

Equations
  • Units.instNeg = { neg := fun (u : αˣ) => { val := -u, inv := -u⁻¹, val_inv := , inv_val := } }
@[simp]
theorem Units.val_neg {α : Type u} [Monoid α] [HasDistribNeg α] (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} [Monoid α] [HasDistribNeg α] :
(-1) = -1
Equations
theorem Units.neg_divp {α : Type u} [Monoid α] [HasDistribNeg α] (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
@[simp]
theorem Units.map_neg {α : Type u} {β : Type v} [Ring α] {F : Type u_1} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) (u : αˣ) :
(Units.map f) (-u) = -(Units.map f) u
theorem Units.map_neg_one {α : Type u} {β : Type v} [Ring α] {F : Type u_1} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) :
(Units.map f) (-1) = -1
theorem IsUnit.neg {α : Type u} [Monoid α] [HasDistribNeg α] {a : α} :
IsUnit aIsUnit (-a)
@[simp]
theorem IsUnit.neg_iff {α : Type u} [Monoid α] [HasDistribNeg α] (a : α) :
theorem isUnit_neg_one {α : Type u} [Monoid α] [HasDistribNeg α] :
IsUnit (-1)
theorem IsUnit.sub_iff {α : Type u} [Ring α] {x : α} {y : α} :
IsUnit (x - y) IsUnit (y - x)
theorem Units.divp_add_divp {α : Type u} [CommRing α] (a : α) (b : α) (u₁ : αˣ) (u₂ : αˣ) :
a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂)
theorem Units.divp_sub_divp {α : Type u} [CommRing α] (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)