English
For n ≠ 0, a ∣ b^n if and only if ceilRoot n a ∣ b.
Русский
Для n ≠ 0 верно: a делится на b^n тогда и только тогда, когда ceilRoot n a делится на b.
LaTeX
$$$ \forall a,b,n \in \mathbb{N}, n \neq 0 \implies a \mid b^n \iff \operatorname{ceilRoot}(n,a) \mid b $$$
Lean4
/-- Galois connection between `ceilRoot n : ℕ → ℕ` and `a ↦ a ^ n : ℕ → ℕ` where `ℕ` is ordered
by divisibility.
Note that this cannot possibly hold for `n = 0`, regardless of the value of `ceilRoot 0 a`, because
the statement reduces to `a = 1 ↔ ceilRoot 0 a ∣ b`, which is false for e.g. `a = 0`,
`b = ceilRoot 0 a`. -/
theorem dvd_pow_iff_ceilRoot_dvd (hn : n ≠ 0) : a ∣ b ^ n ↔ ceilRoot n a ∣ b :=
by
obtain rfl | ha := eq_or_ne a 0
· aesop
obtain rfl | hb := eq_or_ne b 0
· simp [hn]
rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb), ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb,
factorization_pow, factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
