by_cases h : ringChar R = 0
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)