pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left

English

For any x,y,p,k in a CancelCommMonoidWithZero, if y is squarefree and p is prime and p^{k+1} divides x y, then p^k divides x.

Русский

Для любых x,y,p,k в CancelCommMonoidWithZero, если y квадратно свободно, p — простое, и p^{k+1} делит xy, то p^k делит x.

LaTeX

$$$\forall x,y,p,k:\; (\operatorname{Squarefree}(y) \land \operatorname{Prime}(p) \land p^{k+1} \mid x y) \Rightarrow p^k \mid x$$$

Lean4

theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {k : ℕ} (hy : Squarefree y) (hp : Prime p)
    (h : p ^ (k + 1) ∣ x * y) : p ^ k ∣ x := by
  rw [mul_comm] at h
  exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h

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