English
For natural numbers a,n,b, a^n divides b iff a divides floorRoot n b.
Русский
Для натуральных a,n,b: a^n делит b тогда и только тогда, когда a делит floorRoot(n,b).
LaTeX
$$$a^n \mid b \iff a \mid \text{floorRoot}(n,b)$$$
Lean4
/-- Galois connection between `a ↦ a ^ n : ℕ → ℕ` and `floorRoot n : ℕ → ℕ` where `ℕ` is ordered
by divisibility. -/
theorem pow_dvd_iff_dvd_floorRoot : a ^ n ∣ b ↔ a ∣ floorRoot n b :=
by
obtain rfl | hn := eq_or_ne n 0
· simp
obtain rfl | hb := eq_or_ne b 0
· simp
obtain rfl | ha := eq_or_ne a 0
· simp [hn]
rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb, ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩),
factorization_pow, factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
