div_div — Mathlib

English

Let x,y,z ∈ R with y|x and z | (x/y). Then x/y/z = x/(y·z).

Русский

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

LaTeX

$$$$ (y \\mid x) \\land (z \\mid (x / y)) \\Rightarrow \\dfrac{\\dfrac{x}{y}}{z} = \\dfrac{x}{y z}. $$$$

Lean4

theorem div_div {x y z : R} (h1 : y ∣ x) (h2 : z ∣ (x / y)) : x / y / z = x / (y * z) :=
  by
  rcases eq_or_ne y 0 with rfl | hy
  · simp only [div_zero, zero_div, zero_mul]
  rw [← mul_dvd_mul_iff_left hy, EuclideanDomain.mul_div_cancel' hy h1] at h2
  exact (div_mul h1 h2).symm

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