pow_dvd_of_dvd_mul_right — Mathlib

English

Symmetric to Left-Divisibility: If p is prime and p^n ∣ a b with p ∤ b, then p^n ∣ a.

Русский

Симметрично левому случаю: если p простое и p^n делит a b при p не делит b, то p^n делит a.

LaTeX

$$$\\text{Prime}(p) \\Rightarrow \\forall n:\\, \\mathbb{N},\\; (p \\nmid b) \\land (p^n \\mid a b) \\Rightarrow p^n \\mid a.$$$

Lean4

theorem pow_dvd_of_dvd_mul_right [CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p) (n : ℕ) (h : ¬p ∣ b)
    (h' : p ^ n ∣ a * b) : p ^ n ∣ a := by
  rw [mul_comm] at h'
  exact hp.pow_dvd_of_dvd_mul_left n h h'

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