Documentation

Mathlib.Algebra.Ring.Units

Units in semirings and rings #

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

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

Equations
    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.instHasDistribNeg {α : 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} [Semiring α] (a b : α) (u : αˣ) :
      a /ₚ u + b /ₚ u = (a + b) /ₚ u
      source
      theorem Units.add_divp {α : Type u} [Semiring α] (a b : α) (u : αˣ) :
      a + b /ₚ u = (a * ↑u + b) /ₚ u
      source
      theorem Units.divp_add {α : Type u} [Semiring α] (a b : α) (u : αˣ) :
      a /ₚ u + b = (a + b * ↑u) /ₚ u
      source
      theorem Units.divp_sub_divp_same {α : Type u} [Ring α] (a b : α) (u : αˣ) :
      a /ₚ u - b /ₚ u = (a - b) /ₚ u
      source
      theorem Units.sub_divp {α : Type u} [Ring α] (a b : α) (u : αˣ) :
      a - b /ₚ u = (a * ↑u - b) /ₚ 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 : αˣ) :
      (map ↑f) (-u) = -(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) :
      (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} [CommSemiring α] (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)
      source
      theorem RingHom.isUnit_map {α : Type u} {β : Type v} [Semiring α] [Semiring β] (f : α →+* β) {a : α} :
      IsUnit a → IsUnit (f a)