dvd_of_forall_prime_mul_dvd — Mathlib

English

If for all primes p, p | a implies p·a | b, then a | b.

Русский

Если для всех простых p из условия следует, что p делит a влечет p·a делит b, то a делит b.

LaTeX

$$$$ \left( \forall p, \operatorname{Prime}(p) \rightarrow (p \mid a \Rightarrow p \cdot a \mid b) \right) \Rightarrow a \mid b. $$$$

Lean4

theorem dvd_of_forall_prime_mul_dvd {a b : ℕ} (hdvd : ∀ p : ℕ, p.Prime → p ∣ a → p * a ∣ b) : a ∣ b :=
  by
  obtain rfl | ha := eq_or_ne a 1
  · apply one_dvd
  obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
  exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)

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