Units in semirings and rings #

source

ink

instance Units.instNegUnits {α : Type u} [inst : Monoid α] [inst : 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 := (_ : -↑u * -↑u⁻¹ = 1), inv_val := (_ : -↑u⁻¹ * -↑u = 1) } }

source

ink

@[simp]

theorem Units.val_neg {α : Type u} [inst : Monoid α] [inst : 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

ink

@[simp]

theorem Units.coe_neg_one {α : Type u} [inst : Monoid α] [inst : HasDistribNeg α] :

↑(-1) = -1

source

ink

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

HasDistribNeg αˣ

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem Units.neg_divp {α : Type u} [inst : Monoid α] [inst : HasDistribNeg α] (a : α) (u : αˣ) :

-(a /ₚ u) = -a /ₚ u

source

ink

theorem Units.divp_add_divp_same {α : Type u} [inst : Ring α] (a : α) (b : α) (u : αˣ) :

a /ₚ u + b /ₚ u = (a + b) /ₚ u

source

ink

theorem Units.divp_sub_divp_same {α : Type u} [inst : Ring α] (a : α) (b : α) (u : αˣ) :

a /ₚ u - b /ₚ u = (a - b) /ₚ u

source

ink

theorem Units.add_divp {α : Type u} [inst : Ring α] (a : α) (b : α) (u : αˣ) :

a + b /ₚ u = (a * ↑u + b) /ₚ u

source

ink

theorem Units.sub_divp {α : Type u} [inst : Ring α] (a : α) (b : α) (u : αˣ) :

a - b /ₚ u = (a * ↑u - b) /ₚ u

source

ink

theorem Units.divp_add {α : Type u} [inst : Ring α] (a : α) (b : α) (u : αˣ) :

a /ₚ u + b = (a + b * ↑u) /ₚ u

source

ink

theorem Units.divp_sub {α : Type u} [inst : Ring α] (a : α) (b : α) (u : αˣ) :

a /ₚ u - b = (a - b * ↑u) /ₚ u

source

ink

theorem IsUnit.neg {α : Type u} [inst : Monoid α] [inst : HasDistribNeg α] {a : α} :

IsUnit a → IsUnit (-a)

source

ink

@[simp]

theorem IsUnit.neg_iff {α : Type u} [inst : Monoid α] [inst : HasDistribNeg α] (a : α) :

IsUnit (-a) ↔ IsUnit a

source

ink

theorem IsUnit.sub_iff {α : Type u} [inst : Ring α] {x : α} {y : α} :

IsUnit (x - y) ↔ IsUnit (y - x)

source

ink

theorem Units.divp_add_divp {α : Type u} [inst : CommRing α] (a : α) (b : α) (u₁ : αˣ) (u₂ : αˣ) :

a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)

source

ink

theorem Units.divp_sub_divp {α : Type u} [inst : CommRing α] (a : α) (b : α) (u₁ : αˣ) (u₂ : αˣ) :

a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)

source

ink

theorem Units.add_eq_mul_one_add_div {R : Type x} [inst : Semiring R] {a : Rˣ} {b : R} :

↑a + b = ↑a * (1 + ↑a⁻¹ * b)