toClass_zero

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Affine.Point.toClass_zero

English

For a nonsingular h, toClass(some h) equals the class of XYIdeal'(h).

Русский

Для невырожденного h toClass(some h) равен классу XYIdeal'(h).

LaTeX

$$toClass(some h) = [XYIdeal'(h)]$$

Lean4

theorem toClass_zero : toClass (0 : W.Point) = 0 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru