English
A noncomputable version of floorRoot expresses floorRoot(n,a) as the product over primes p of p^(⎣v_p(a)/n⎦) when n>0 and a>0, otherwise 0.
Русский
Непрямым образом floorRoot(n,a) равен произведению p^(⌊v_p(a)/n⌋) по всем простым p при условии n>0 и a>0, иначе 0.
LaTeX
$$$\text{floorRoot}(n,a) = \begin{cases}0, & n=0 \lor a=0, \\ \prod_{p} p^{\left\lfloor \dfrac{v_p(a)}{n} \right\rfloor}, & \text{иначе}.\end{cases}$$$
Lean4
/-- The RHS is a noncomputable version of `Nat.floorRoot` with better order-theoretic
properties. -/
theorem floorRoot_def : floorRoot n a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod (· ^ ·) := by
unfold floorRoot; split_ifs with h <;> simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]
