div_eq_iff_eq_mul_of_dvd — Mathlib

English

Let y ≠ 0 and y ∣ x. Then x/y = z if and only if x = y·z.

Русский

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

LaTeX

$$$$ y \\neq 0 \\ \\land\\ y \\mid x \\Rightarrow (x/y = z \\iff x = y \\cdot z). $$$$

Lean4

theorem div_eq_iff_eq_mul_of_dvd (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : x / y = z ↔ x = y * z :=
  by
  obtain ⟨a, ha⟩ := h2
  rw [ha, mul_div_cancel_left₀ _ h1]
  simp only [mul_eq_mul_left_iff, h1, or_false]

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