div_mul — Mathlib

English

Let R be a Euclidean domain and suppose y divides x and y·z divides x. Then x is divisible by y·z and the quotient satisfies x/(y·z) = (x/y)/z.

Русский

Пусть R — евклидово кольцо. Пусть y делит x и y·z делит x. Тогда x делится на y·z и x/(y·z) = (x/y)/z.

LaTeX

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

Lean4

theorem div_mul {x y z : R} (h1 : y ∣ x) (h2 : y * z ∣ x) : x / (y * z) = x / y / z :=
  by
  rcases eq_or_ne z 0 with rfl | hz
  · simp only [mul_zero, div_zero]
  apply eq_div_of_mul_eq_right hz
  rw [← EuclideanDomain.mul_div_assoc z h2, mul_comm y z, mul_div_mul_cancel hz h1]

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