integralModel — Mathlib

English

There is an additive equivalence between projective and affine points that preserves addition, with consistent left and right inverses.

Русский

Существует эквивалентность по сложению между проективными и аффинными точками, сохраняющая сложение; отображение имеет корректные левые и правые обратные.

LaTeX

$$$\\text{toAffineAddEquiv} : W.Point \\simeq_+ W.toAffine.Point$$$

Lean4

/-- An integral model of an integral Weierstrass curve. -/
noncomputable def integralModel (W : WeierstrassCurve K) [hW : IsIntegral R W] : WeierstrassCurve R :=
  hW.integral.choose

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