Theorem: ValidModel.iso_rst_val_discr_to_nat (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
r s t : R
e : ValidModel R
⊢ val_discr_to_nat valp (rst_iso r s t e) = val_discr_to_nat valp e
Tactic:
simp [val_discr_to_nat]
State after:
no goals