squarefree — Mathlib

English

If y is squarefree and p is prime and p^(k+1) divides x·y, then p^k divides x.

Русский

Если y квадратно свободно, и p — простое, и p^(k+1) делит x·y, тогда p^k делит x.

LaTeX

$$$\\text{Squarefree}(y) \\to \\text{Prime}(p) \\to (p^{k+1} \\mid x y) \\Rightarrow p^{k} \\mid x.$$$

Lean4

theorem squarefree (h0 : x ≠ 0) (h : IsRadical x) : Squarefree x :=
  by
  rintro z ⟨w, rfl⟩
  specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩
  rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h
  rw [mul_assoc, mul_ne_zero_iff] at h0; exact h0.2

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