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