English
The noncomputable version of ceilRoot states that ceilRoot(n,a) equals 0 if n=0 or a=0, otherwise the product over primes p of p^{ceil(v_p(a)/n)}.
Русский
Не вычислимая версия ceilRoot(n,a) равна 0 при n=0 или a=0, иначе равно произведению по всем простым p: p^{ceil(v_p(a)/n)}.
LaTeX
$$$\text{ceilRoot}(n,a) = \begin{cases}0, & n=0 \lor a=0, \\ \prod_{p} p^{\left\lceil \dfrac{v_p(a)}{n} \right\rceil}, & \text{иначе}.\end{cases}$$$
Lean4
/-- The RHS is a noncomputable version of `Nat.ceilRoot` with better order-theoretic
properties. -/
theorem ceilRoot_def : ceilRoot n a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod (· ^ ·) :=
by
unfold ceilRoot
split_ifs with h <;> simp [Finsupp.ceilDiv_def, prod_mapRange_index pow_zero, Nat.ceilDiv_eq_add_pred_div]
