pow_dvd_of_pow_dvd — Mathlib

English

If y is squarefree and x^n divides y, then x^n divides x.

Русский

Если y квадратно свободно и x^n делит y, тогда x^n делит x.

LaTeX

$$$\mathrm{Squarefree}(y) \land x^{n} \mid y \rightarrow x^{n} \mid x$$$

Lean4

theorem pow_dvd_of_pow_dvd [Monoid R] {x y : R} {n : ℕ} (hx : Squarefree y) (h : x ^ n ∣ y) : x ^ n ∣ x :=
  by
  by_cases hu : IsUnit x
  · exact (hu.pow n).dvd
  · rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl <;> simp

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