English
The floorRoot operation aligns with prime valuations by dividing exponents by n and taking the product of p^(⎣e_p(a)/n⎦).
Русский
Операция floorRoot сохраняет нормы по простым факторам: степени в факторизации делятся на n с округлением вниз и далее перемножаются.
LaTeX
$$$(n,a) \mapsto (a.generic\_factorization) \;\text{and} \; (a.factorization \ ⌊/⌋ n)$, i.e. the prime exponents of floorRoot(n,a) are ⌊v_p(a)/n⌋.$$
Lean4
/-- Flooring root of a natural number. This divides the valuation of every prime number rounding
down.
Eg if `n = 2`, `a = 2^3 * 3^2 * 5`, then `floorRoot n a = 2 * 3`.
In order theory terms, this is the upper or right adjoint of the map `a ↦ a ^ n : ℕ → ℕ` where `ℕ`
is ordered by divisibility.
To ensure that the adjunction (`Nat.pow_dvd_iff_dvd_floorRoot`) holds in as many cases as possible,
we special-case the following values:
* `floorRoot 0 a = 0`
* `floorRoot n 0 = 0`
-/
def floorRoot (n a : ℕ) : ℕ :=
if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ (k / n)
