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

State before:
R : Type u
inst✝ : CommRing R
P : R × R
⊢ var_change 0 0 0 P = P
Tactic:
simp [var_change]
State after:
no goals