div_eq_div_iff_mul_eq_mul_of_dvd — Mathlib

English

Let x,y,z,t ∈ R with y ≠ 0, t ≠ 0, y ∣ x, t ∣ z. Then x/y = z/t if and only if t·x = y·z.

Русский

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

LaTeX

$$$$ {R} \\text{ with } y \\neq 0, \\ t \\neq 0, y \\mid x, t \\mid z \\Rightarrow \\dfrac{x}{y} = \\dfrac{z}{t} \\iff t \\cdot x = y \\cdot z. $$$$

Lean4

theorem div_eq_div_iff_mul_eq_mul_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 :=
  by
  rw [div_eq_iff_eq_mul_of_dvd _ _ _ h1 h3, ← mul_div_assoc _ h4, eq_div_iff_mul_eq_of_dvd _ _ _ h2]
  obtain ⟨a, ha⟩ := h4
  use y * a
  rw [ha, mul_comm, mul_assoc, mul_comm y a]

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