zero_point

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Jacobian.Point.zero_point

English

The zero point is represented by the vector [1,1,0] in the standard quotient representation.

Русский

Нулевая точка представлена в стандартной факторной записи вектором [1,1,0].

LaTeX

$$(0 : W'.Point).point = ⟦![1, 1, 0]⟧$$

Lean4

theorem zero_point [Nontrivial R] : (0 : W'.Point).point = ⟦![1, 1, 0]⟧ :=
  rfl

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

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

Разделы

Аффилиация

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