left_dvd_or_dvd_right_of_dvd_mul — Mathlib

English

In a CancelMonoidWithZero M, if p is prime and a divides p·b, then p divides a or a divides b.

Русский

В CancelMonoidWithZero M, если p простое и a делит p·b, то p делит a или a делит b.

LaTeX

$$$\\forall a,b:\\, M,\\; \\operatorname{Prime}(p) \\Rightarrow (a \\mid p b \\Rightarrow (p \\mid a) \\lor (a \\mid b)).$$$

Lean4

theorem left_dvd_or_dvd_right_of_dvd_mul [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) {a b : M} :
    a ∣ p * b → p ∣ a ∨ a ∣ b := by
  rintro ⟨c, hc⟩
  rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)
  · exact Or.inl h
  · rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
    exact Or.inr (hc.symm ▸ dvd_mul_right _ _)

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