. exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
no goals