Units in semirings and rings

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 := ⋯ } }

@[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

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

Equations

• Units.instHasDistribNegUnitsToMulInstMulOneClass = Function.Injective.hasDistribNeg Units.val ⋯ ⋯ ⋯

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 a → IsUnit (-a)

@[simp]

theorem IsUnit.neg_iff {α : Type u} [Monoid α] [HasDistribNeg α] (a : α) : IsUnit (-a) ↔ IsUnit 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)