Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland

! This file was ported from Lean 3 source module algebra.ring.units
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Ring.InjSurj
import Mathlib.Algebra.Group.Units

/-!
# Units in semirings and rings

-/

universe u v w x

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} {γ: Type wγ : Type w: Type (w+1)Type w} {R: Type xR : Type x: Type (x+1)Type x}

open Function

namespace Units

section HasDistribNeg

variable [Monoid: Type ?u.18 → Type ?u.18Monoid α: Type uα] [HasDistribNeg: (α : Type ?u.1880) → [inst : Mul α] → Type ?u.1880HasDistribNeg α: Type uα] {a: αa b: αb : α: Type uα}

/-- Each element of the group of units of a ring has an additive inverse. -/
instance: {α : Type u} → [inst : Monoid α] → [inst_1 : HasDistribNeg α] → Neg αˣinstance : Neg: Type ?u.422 → Type ?u.422Neg α: Type uαˣ :=
⟨fun u: ?m.440u => ⟨-↑u: ?m.440u, -↑u: ?m.440u⁻¹, byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wR: Type xinst✝¹: Monoid αinst✝: HasDistribNeg αa, b: αu: αˣ-↑u * -↑u⁻¹ = 1simpGoals accomplished! 🐙, byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wR: Type xinst✝¹: Monoid αinst✝: HasDistribNeg αa, b: αu: αˣ-↑u⁻¹ * -↑u = 1simpGoals accomplished! 🐙⟩⟩

/-- 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, norm_cast]
protected theorem val_neg: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (u : αˣ), ↑(-u) = -↑uval_neg (u: αˣu : α: Type uαˣ) : (↑(-u: αˣu) : α: Type uα) = -u: αˣu :=
rfl: ∀ {α : Sort ?u.2876} {a : α}, a = arfl
#align units.coe_neg Units.val_neg: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (u : αˣ), ↑(-u) = -↑uUnits.val_neg

@[simp, norm_cast]
protected theorem coe_neg_one: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α], ↑(-1) = -1coe_neg_one : ((-1: ?m.31811 : α: Type uαˣ) : α: Type uα) = -1: ?m.35721 :=
rfl: ∀ {α : Sort ?u.3984} {a : α}, a = arfl
#align units.coe_neg_one Units.coe_neg_one: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α], ↑(-1) = -1Units.coe_neg_one

instance: {α : Type u} → [inst : Monoid α] → [inst_1 : HasDistribNeg α] → HasDistribNeg αˣinstance : HasDistribNeg: (α : Type ?u.4284) → [inst : Mul α] → Type ?u.4284HasDistribNeg α: Type uαˣ :=
Units.ext: ∀ {α : Type ?u.4478} [inst : Monoid α], Injective valUnits.ext.hasDistribNeg: {α : Type ?u.4489} →
{β : Type ?u.4488} →
[inst : Mul α] →
[inst_1 : HasDistribNeg α] →
[inst_2 : Neg β] →
[inst_3 : Mul β] →
(f : β → α) →
Injective f → (∀ (a : β), f (-a) = -f a) → (∀ (a b : β), f (a * b) = f a * f b) → HasDistribNeg βhasDistribNeg _: ?m.4501 → ?m.4500_ Units.val_neg: ∀ {α : Type ?u.4727} [inst : Monoid α] [inst_1 : HasDistribNeg α] (u : αˣ), ↑(-u) = -↑uUnits.val_neg Units.val_mul: ∀ {α : Type ?u.4904} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑bUnits.val_mul

@[field_simps]
theorem neg_divp: ∀ (a : α) (u : αˣ), -(a /ₚ u) = -a /ₚ uneg_divp (a: αa : α: Type uα) (u: αˣu : α: Type uαˣ) : -(a: αa /ₚ u: αˣu) = -a: αa /ₚ u: αˣu := byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wR: Type xinst✝¹: Monoid αinst✝: HasDistribNeg αa✝, b, a: αu: αˣ-(a /ₚ u) = -a /ₚ usimp only [divp: {α : Type ?u.5535} → [inst : Monoid α] → α → αˣ → αdivp, neg_mul: ∀ {α : Type ?u.5541} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * b = -(a * b)neg_mul]Goals accomplished! 🐙
#align units.neg_divp Units.neg_divp: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α) (u : αˣ), -(a /ₚ u) = -a /ₚ uUnits.neg_divp

end HasDistribNeg

section Ring

variable [Ring: Type ?u.5862 → Type ?u.5862Ring α: Type uα] {a: αa b: αb : α: Type uα}

-- Needs to have higher simp priority than divp_add_divp. 1000 is the default priority.
@[field_simps 1010]
theorem divp_add_divp_same: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u + b /ₚ u = (a + b) /ₚ udivp_add_divp_same (a: αa b: αb : α: Type uα) (u: αˣu : α: Type uαˣ) : a: αa /ₚ u: αˣu + b: αb /ₚ u: αˣu = (a: αa + b: αb) /ₚ u: αˣu := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u + b /ₚ u = (a + b) /ₚ usimp only [divp: {α : Type ?u.6069} → [inst : Monoid α] → α → αˣ → αdivp, add_mul: ∀ {R : Type ?u.6075} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul]Goals accomplished! 🐙
#align units.divp_add_divp_same Units.divp_add_divp_same: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u + b /ₚ u = (a + b) /ₚ uUnits.divp_add_divp_same

-- Needs to have higher simp priority than divp_sub_divp. 1000 is the default priority.
@[field_simps 1010]
theorem divp_sub_divp_same: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u - b /ₚ u = (a - b) /ₚ udivp_sub_divp_same (a: αa b: αb : α: Type uα) (u: αˣu : α: Type uαˣ) : a: αa /ₚ u: αˣu - b: αb /ₚ u: αˣu = (a: αa - b: αb) /ₚ u: αˣu := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b /ₚ u = (a - b) /ₚ urw [α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b /ₚ u = (a - b) /ₚ usub_eq_add_neg: ∀ {G : Type ?u.6519} [inst : SubNegMonoid G] (a b : G), a - b = a + -bsub_eq_add_neg,α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u + -(b /ₚ u) = (a - b) /ₚ u α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b /ₚ u = (a - b) /ₚ usub_eq_add_neg: ∀ {G : Type ?u.6581} [inst : SubNegMonoid G] (a b : G), a - b = a + -bsub_eq_add_neg,α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u + -(b /ₚ u) = (a + -b) /ₚ u α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b /ₚ u = (a - b) /ₚ uneg_divp: ∀ {α : Type ?u.6615} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α) (u : αˣ), -(a /ₚ u) = -a /ₚ uneg_divp,α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u + -b /ₚ u = (a + -b) /ₚ u α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b /ₚ u = (a - b) /ₚ udivp_add_divp_same: ∀ {α : Type ?u.6727} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u + b /ₚ u = (a + b) /ₚ udivp_add_divp_sameα: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣ(a + -b) /ₚ u = (a + -b) /ₚ u]Goals accomplished! 🐙
#align units.divp_sub_divp_same Units.divp_sub_divp_same: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u - b /ₚ u = (a - b) /ₚ uUnits.divp_sub_divp_same

@[field_simps]
theorem add_divp: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a + b /ₚ u = (a * ↑u + b) /ₚ uadd_divp (a: αa b: αb : α: Type uα) (u: αˣu : α: Type uαˣ) : a: αa + b: αb /ₚ u: αˣu = (a: αa * u: αˣu + b: αb) /ₚ u: αˣu := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa + b /ₚ u = (a * ↑u + b) /ₚ usimp only [divp: {α : Type ?u.7402} → [inst : Monoid α] → α → αˣ → αdivp, add_mul: ∀ {R : Type ?u.7408} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul, Units.mul_inv_cancel_right: ∀ {α : Type ?u.7436} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b * ↑b⁻¹ = aUnits.mul_inv_cancel_right]Goals accomplished! 🐙
#align units.add_divp Units.add_divp: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a + b /ₚ u = (a * ↑u + b) /ₚ uUnits.add_divp

@[field_simps]
theorem sub_divp: ∀ (a b : α) (u : αˣ), a - b /ₚ u = (a * ↑u - b) /ₚ usub_divp (a: αa b: αb : α: Type uα) (u: αˣu : α: Type uαˣ) : a: αa - b: αb /ₚ u: αˣu = (a: αa * u: αˣu - b: αb) /ₚ u: αˣu := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa - b /ₚ u = (a * ↑u - b) /ₚ usimp only [divp: {α : Type ?u.8287} → [inst : Monoid α] → α → αˣ → αdivp, sub_mul: ∀ {α : Type ?u.8293} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * csub_mul, Units.mul_inv_cancel_right: ∀ {α : Type ?u.8317} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b * ↑b⁻¹ = aUnits.mul_inv_cancel_right]Goals accomplished! 🐙
#align units.sub_divp Units.sub_divp: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a - b /ₚ u = (a * ↑u - b) /ₚ uUnits.sub_divp

@[field_simps]
theorem divp_add: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u + b = (a + b * ↑u) /ₚ udivp_add (a: αa b: αb : α: Type uα) (u: αˣu : α: Type uαˣ) : a: αa /ₚ u: αˣu + b: αb = (a: αa + b: αb * u: αˣu) /ₚ u: αˣu := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u + b = (a + b * ↑u) /ₚ usimp only [divp: {α : Type ?u.9156} → [inst : Monoid α] → α → αˣ → αdivp, add_mul: ∀ {R : Type ?u.9162} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul, Units.mul_inv_cancel_right: ∀ {α : Type ?u.9190} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b * ↑b⁻¹ = aUnits.mul_inv_cancel_right]Goals accomplished! 🐙
#align units.divp_add Units.divp_add: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u + b = (a + b * ↑u) /ₚ uUnits.divp_add

@[field_simps]
theorem divp_sub: ∀ (a b : α) (u : αˣ), a /ₚ u - b = (a - b * ↑u) /ₚ udivp_sub (a: αa b: αb : α: Type uα) (u: αˣu : α: Type uαˣ) : a: αa /ₚ u: αˣu - b: αb = (a: αa - b: αb * u: αˣu) /ₚ u: αˣu := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b = (a - b * ↑u) /ₚ usimp only [divp: {α : Type ?u.10037} → [inst : Monoid α] → α → αˣ → αdivp, sub_mul: ∀ {α : Type ?u.10043} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * csub_mul, sub_right_inj: ∀ {G : Type ?u.10067} [inst : AddGroup G] {a b c : G}, a - b = a - c ↔ b = csub_right_inj]α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b * ↑u * ↑u⁻¹
α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣa /ₚ u - b = (a - b * ↑u) /ₚ urw [α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b * ↑u * ↑u⁻¹mul_assoc: ∀ {G : Type ?u.10319} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b * (↑u * ↑u⁻¹) α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b * ↑u * ↑u⁻¹Units.mul_inv: ∀ {α : Type ?u.10475} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1Units.mul_inv,α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b * 1 α: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b * ↑u * ↑u⁻¹mul_one: ∀ {M : Type ?u.10578} [inst : MulOneClass M] (a : M), a * 1 = amul_oneα: Type uβ: Type vγ: Type wR: Type xinst✝: Ring αa✝, b✝, a, b: αu: αˣb = b]Goals accomplished! 🐙
#align units.divp_sub Units.divp_sub: ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u - b = (a - b * ↑u) /ₚ uUnits.divp_sub

end Ring

end Units

theorem IsUnit.neg: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : α}, IsUnit a → IsUnit (-a)IsUnit.neg [Monoid: Type ?u.10674 → Type ?u.10674Monoid α: Type uα] [HasDistribNeg: (α : Type ?u.10677) → [inst : Mul α] → Type ?u.10677HasDistribNeg α: Type uα] {a: αa : α: Type uα} : IsUnit: {M : Type ?u.10871} → [inst : Monoid M] → M → PropIsUnit a: αa → IsUnit: {M : Type ?u.10888} → [inst : Monoid M] → M → PropIsUnit (-a: αa)
| ⟨x: αˣx, hx: ↑x = ahx⟩ => hx: ↑x = ahx ▸ (-x: αˣx).isUnit: ∀ {M : Type ?u.11203} [inst : Monoid M] (u : Mˣ), IsUnit ↑uisUnit
#align is_unit.neg IsUnit.neg: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : α}, IsUnit a → IsUnit (-a)IsUnit.neg

@[simp]
theorem IsUnit.neg_iff: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α), IsUnit (-a) ↔ IsUnit aIsUnit.neg_iff [Monoid: Type ?u.11308 → Type ?u.11308Monoid α: Type uα] [HasDistribNeg: (α : Type ?u.11311) → [inst : Mul α] → Type ?u.11311HasDistribNeg α: Type uα] (a: αa : α: Type uα) : IsUnit: {M : Type ?u.11504} → [inst : Monoid M] → M → PropIsUnit (-a: αa) ↔ IsUnit: {M : Type ?u.11762} → [inst : Monoid M] → M → PropIsUnit a: αa :=
⟨fun h: ?m.11778h => neg_neg: ∀ {G : Type ?u.11780} [inst : InvolutiveNeg G] (a : G), - -a = aneg_neg a: αa ▸ h: ?m.11778h.neg: ∀ {α : Type ?u.11931} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : α}, IsUnit a → IsUnit (-a)neg, IsUnit.neg: ∀ {α : Type ?u.11960} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : α}, IsUnit a → IsUnit (-a)IsUnit.neg⟩
#align is_unit.neg_iff IsUnit.neg_iff: ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α), IsUnit (-a) ↔ IsUnit aIsUnit.neg_iff

theorem IsUnit.sub_iff: ∀ [inst : Ring α] {x y : α}, IsUnit (x - y) ↔ IsUnit (y - x)IsUnit.sub_iff [Ring: Type ?u.12022 → Type ?u.12022Ring α: Type uα] {x: αx y: αy : α: Type uα} : IsUnit: {M : Type ?u.12029} → [inst : Monoid M] → M → PropIsUnit (x: αx - y: αy) ↔ IsUnit: {M : Type ?u.12114} → [inst : Monoid M] → M → PropIsUnit (y: αy - x: αx) :=
(IsUnit.neg_iff: ∀ {α : Type ?u.12148} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α), IsUnit (-a) ↔ IsUnit aIsUnit.neg_iff _: ?m.12149_).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans <| neg_sub: ∀ {α : Type ?u.12264} [inst : SubtractionMonoid α] (a b : α), -(a - b) = b - aneg_sub x: αx y: αy ▸ Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_unit.sub_iff IsUnit.sub_iff: ∀ {α : Type u} [inst : Ring α] {x y : α}, IsUnit (x - y) ↔ IsUnit (y - x)IsUnit.sub_iff

namespace Units

@[field_simps]
theorem divp_add_divp: ∀ [inst : CommRing α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)divp_add_divp [CommRing: Type ?u.12317 → Type ?u.12317CommRing α: Type uα] (a: αa b: αb : α: Type uα) (u₁: αˣu₁ u₂: αˣu₂ : α: Type uαˣ) :
a: αa /ₚ u₁: αˣu₁ + b: αb /ₚ u₂: αˣu₂ = (a: αa * u₂: αˣu₂ + u₁: αˣu₁ * b: αb) /ₚ (u₁: αˣu₁ * u₂: αˣu₂) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)simp only [divp: {α : Type ?u.13588} → [inst : Monoid α] → α → αˣ → αdivp, add_mul: ∀ {R : Type ?u.13594} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul, mul_inv_rev: ∀ {G : Type ?u.13622} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹mul_inv_rev, val_mul: ∀ {α : Type ?u.13641} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑bval_mul]α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)
α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)rw [α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)mul_comm: ∀ {G : Type ?u.14119} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm (↑u₁: αˣu₁ * b: αb),α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)mul_comm: ∀ {G : Type ?u.14353} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm b: αbα: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)]α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)
α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)rw [α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)←mul_assoc: ∀ {G : Type ?u.14375} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * ↑u₂⁻¹ * ↑u₁⁻¹ + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)←mul_assoc: ∀ {G : Type ?u.14476} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * ↑u₂⁻¹ * ↑u₁⁻¹ + ↑u₂⁻¹ * ↑u₁⁻¹ * ↑u₁ * b α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)mul_assoc: ∀ {G : Type ?u.14552} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc a: αa,α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * (↑u₂ * ↑u₂⁻¹) * ↑u₁⁻¹ + ↑u₂⁻¹ * ↑u₁⁻¹ * ↑u₁ * b α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)mul_assoc: ∀ {G : Type ?u.14563} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc (↑u₂: αˣu₂⁻¹ : α: Type uα),α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * (↑u₂ * ↑u₂⁻¹) * ↑u₁⁻¹ + ↑u₂⁻¹ * (↑u₁⁻¹ * ↑u₁) * b α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)mul_inv: ∀ {α : Type ?u.14739} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1mul_inv,α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * 1 * ↑u₁⁻¹ + ↑u₂⁻¹ * (↑u₁⁻¹ * ↑u₁) * b α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)inv_mul: ∀ {α : Type ?u.14806} [inst : Monoid α] (a : αˣ), ↑a⁻¹ * ↑a = 1inv_mul,α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * 1 * ↑u₁⁻¹ + ↑u₂⁻¹ * 1 * b α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)mul_one: ∀ {M : Type ?u.14873} [inst : MulOneClass M] (a : M), a * 1 = amul_one,α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₁⁻¹ + ↑u₂⁻¹ * 1 * b
α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)mul_one: ∀ {M : Type ?u.14929} [inst : MulOneClass M] (a : M), a * 1 = amul_oneα: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₁⁻¹ + ↑u₂⁻¹ * b]Goals accomplished! 🐙
-- porting note: `assoc_rw` not ported: `assoc_rw [mul_inv, mul_inv, mul_one, mul_one]`
#align units.divp_add_divp Units.divp_add_divp: ∀ {α : Type u} [inst : CommRing α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)Units.divp_add_divp

@[field_simps]
theorem divp_sub_divp: ∀ {α : Type u} [inst : CommRing α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)divp_sub_divp [CommRing: Type ?u.15008 → Type ?u.15008CommRing α: Type uα] (a: αa b: αb : α: Type uα) (u₁: αˣu₁ u₂: αˣu₂ : α: Type uαˣ) :
a: αa /ₚ u₁: αˣu₁ - b: αb /ₚ u₂: αˣu₂ = (a: αa * u₂: αˣu₂ - u₁: αˣu₁ * b: αb) /ₚ (u₁: αˣu₁ * u₂: αˣu₂) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: CommRing αa, b: αu₁, u₂: αˣa /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)simp only [sub_eq_add_neg: ∀ {G : Type ?u.16234} [inst : SubNegMonoid G] (a b : G), a - b = a + -bsub_eq_add_neg, neg_divp: ∀ {α : Type ?u.16250} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α) (u : αˣ), -(a /ₚ u) = -a /ₚ uneg_divp, divp_add_divp: ∀ {α : Type ?u.16269} [inst : CommRing α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)divp_add_divp, mul_neg: ∀ {α : Type ?u.16289} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), a * -b = -(a * b)mul_neg]Goals accomplished! 🐙
#align units.divp_sub_divp Units.divp_sub_divp: ∀ {α : Type u} [inst : CommRing α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)Units.divp_sub_divp

theorem add_eq_mul_one_add_div: ∀ [inst : Semiring R] {a : Rˣ} {b : R}, ↑a + b = ↑a * (1 + ↑a⁻¹ * b)add_eq_mul_one_add_div [Semiring: Type ?u.16742 → Type ?u.16742Semiring R: Type xR] {a: Rˣa : R: Type xRˣ} {b: Rb : R: Type xR} : ↑a: Rˣa + b: Rb = a: Rˣa * (1: ?m.167891 + ↑a: Rˣa⁻¹ * b: Rb) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * (1 + ↑a⁻¹ * b)rw [α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * (1 + ↑a⁻¹ * b)mul_add: ∀ {R : Type ?u.17714} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add,α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * 1 + ↑a * (↑a⁻¹ * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * (1 + ↑a⁻¹ * b)mul_one: ∀ {M : Type ?u.18040} [inst : MulOneClass M] (a : M), a * 1 = amul_one,α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a + ↑a * (↑a⁻¹ * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * (1 + ↑a⁻¹ * b)← mul_assoc: ∀ {G : Type ?u.18091} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a + ↑a * ↑a⁻¹ * b α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * (1 + ↑a⁻¹ * b)Units.mul_inv: ∀ {α : Type ?u.18226} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1Units.mul_inv,α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a + 1 * b α: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a * (1 + ↑a⁻¹ * b)one_mul: ∀ {M : Type ?u.18298} [inst : MulOneClass M] (a : M), 1 * a = aone_mulα: Type uβ: Type vγ: Type wR: Type xinst✝: Semiring Ra: Rˣb: R↑a + b = ↑a + b]Goals accomplished! 🐙