no goals
R : Type ?u.80816
K : Type u_1
L : Type u_2
inst✝² : DivisionRing K
inst✝¹ : Semiring L
inst✝ : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, f.map_zero]