mathlib3 documentation

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.

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

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

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