English
In a commutative semiring, the sum of two divp terms equals a divp of a linear combination: 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_add_divp [CommSemiring α] (a b : α) (u₁ u₂ : αˣ) : a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂) :=
by
simp only [divp, add_mul, mul_inv_rev, val_mul]
rw [mul_comm (↑u₁ * b), mul_comm b]
rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one, mul_one]
-- Porting note: `assoc_rw` not ported: `assoc_rw [mul_inv, mul_inv, mul_one, mul_one]`
