rw [pow_add, pow_mul, pth_root_pow_char h, mul_comm]
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ (n % ringChar R + ringChar R * (n / ringChar R)) = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
no goals