English
CeilRoot divides valuations by rounding up; it is the dual notion to floorRoot with respect to the same divisor order.
Русский
CeilRoot делит значения по принципу округления вверх; это двойственная к floorRoot конструкция в отношении того же порядка делимости.
LaTeX
$$$\text{ceilRoot}(n,a) = 0$ if n=0 or a=0; otherwise $\text{ceilRoot}(n,a)$ divides valuations with ceil instead of floor.$$
Lean4
/-- Ceiling root of a natural number. This divides the valuation of every prime number rounding up.
Eg if `n = 3`, `a = 2^4 * 3^2 * 5`, then `ceilRoot n a = 2^2 * 3 * 5`.
In order theory terms, this is the lower or left adjoint of the map `a ↦ a ^ n : ℕ → ℕ` where `ℕ`
is ordered by divisibility.
To ensure that the adjunction (`Nat.dvd_pow_iff_ceilRoot_dvd`) holds in as many cases as possible,
we special-case the following values:
* `ceilRoot 0 a = 0` (this one is not strictly necessary)
* `ceilRoot n 0 = 0`
-/
def ceilRoot (n a : ℕ) : ℕ :=
if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)
