toClass_injective — Mathlib

English

The class map κ from the affine Weierstrass point set is injective: κ(P)=κ(Q) implies P=Q.

Русский

Отображение класса κ с множества точек аффинной кривой Вейерштрасса инъективно: если κ(P)=κ(Q), то P=Q.

LaTeX

$$$\kappa(P)=\kappa(Q) \Rightarrow P=Q$$$

Lean4

theorem toClass_injective : Function.Injective <| toClass (W := W) :=
  by
  rintro (_ | h) _ hP
  all_goals rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]
  · exact zero_add 0
  · exact CoordinateRing.mk_XYIdeal'_neg_mul h

Похожие утверждения