div_dvd_of_dvd — Mathlib

English

If q ∣ p, then p / q ∣ p (alternative formulation).

Русский

Если q делит p, то p / q делит p (альтернативная формулировка).

LaTeX

$$$ q \mid p \Rightarrow p / q \mid p $$$

Lean4

theorem div_dvd_of_dvd {p q : R} (hpq : q ∣ p) : p / q ∣ p :=
  by
  by_cases hq : q = 0
  · rw [hq, zero_dvd_iff] at hpq
    rw [hpq]
    exact dvd_zero _
  use q
  rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]

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