Theorem: Model.weierstrass_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
⊢ weierstrass (map f e) (Prod.map (↑f) (↑f) P) = ↑f (weierstrass e P)
Tactic:
simp [weierstrass]
State after:
no goals