divp_sub_divp — Mathlib

English

In a commutative ring, the difference of two divp terms equals a divp of a difference: a /ₚ u₁ − b /ₚ u₂ = (a · u₂ − u₁ · b) /ₚ (u₁ · u₂).

Русский

В коммутативном кольце разность двух делений на единицы равна делению разности: a /ₚ u₁ − b /ₚ u₂ = (a · u₂ − u₁ · b) /ₚ (u₁ · u₂).

LaTeX

$$$a /ₚ u_1 - b /ₚ u_2 = (a \\cdot u_2 - u_1 \\cdot b) /ₚ (u_1 \\cdot u_2)$$$

Lean4

theorem divp_sub_divp [CommRing α] (a b : α) (u₁ u₂ : αˣ) : a /ₚ u₁ - b /ₚ u₂ = (a * u₂ - u₁ * b) /ₚ (u₁ * u₂) := by
  simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]

Похожие утверждения