Theorem: Model.dweierstrass_dy_map (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
P : R × R
⊢ dweierstrass_dy (map f e) (Prod.map (↑f) (↑f) P) = ↑f (dweierstrass_dy e P)
Tactic:
simp [dweierstrass_dy]
State after:
no goals