sorry
R✝ : Type u
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ ringChar (R ⧸ SurjVal.ideal evr.valtn) = evr.residue_char
no goals