exact move_singular_point_to_origin e hd
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
hd : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
no goals