Documentation

Mathlib.Algebra.Ring.Units

Units in semirings and rings #

source
instance Units.instNegUnits {α : Type u} [Monoid α] [HasDistribNeg α] :
Neg αˣ

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

Equations
  • Units.instNegUnits = { neg := fun (u : αˣ) => { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } }
source
@[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.

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