Theorem: ENatValRing.key (ECTate/Algebra/ResidueRing.lean)

State before:
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
Tactic:
sorry
State after:
no goals