div_add_div_of_dvd — Mathlib

English

Let x,y,z,t ∈ R with y ≠ 0, t ≠ 0, y|x, t|z. Then x/y + z/t = (t·x + y·z)/(t·y).

Русский

Пусть x,y,z,t ∈ R, y ≠ 0, t ≠ 0, y делит x, t делит z. Тогда x/y + z/t = (t·x + y·z)/(t·y).

LaTeX

$$$$ y \\neq 0 \\ \\land\\ t \\neq 0 \\ \\land\\ y \\mid x \\ \\land\\ t \\mid z \\Rightarrow \\dfrac{x}{y} + \\dfrac{z}{t} = \\dfrac{t x + y z}{t y}. $$$$

Lean4

theorem div_add_div_of_dvd {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) :
    x / y + z / t = (t * x + y * z) / (t * y) :=
  by
  apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
  rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y, mul_assoc,
    EuclideanDomain.mul_div_cancel' h2 h4]

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