English
The equivalence respects the additive structure via its map_add property.
Русский
Эквиваленция сохраняет структуру сложения через свойство map_add.
LaTeX
$$map_add$$
Lean4
noncomputable instance : AddCommGroup W.Point where
nsmul := nsmulRec
zsmul := zsmulRec
zero_add
_ := by
classical
apply (toAffineAddEquiv W).injective
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]
add_zero
_ := by
classical
apply (toAffineAddEquiv W).injective
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]
neg_add_cancel
P := by
classical
apply (toAffineAddEquiv W).injective
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]
add_comm _
_ := by
classical
apply (toAffineAddEquiv W).injective
simp only [map_add, add_comm]
add_assoc _ _
_ := by
classical
apply (toAffineAddEquiv W).injective
simp only [map_add, add_assoc]
