no goals
R : Type u
inst✝⁶ : CommSemiring R
S : Type v
inst✝⁵ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP R p
inst✝² : PerfectRing R p
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
x : R
⊢ ↑(frobenius ((fun x => S) (↑(pthRoot R p) x)) p) (↑f (↑(pthRoot R p) x)) = ↑f x
rw [← f.map_frobenius, frobenius_pthRoot]