addZ_neg

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

Negation preserves nonsingularity: if P is nonsingular, then W.neg P is nonsingular.

Русский

Отрицание сохраняет несингулярность: если P несингулярна, то W.neg P несингулярна.

LaTeX

$$$\forall {P},\ W.Nonsingular P \Rightarrow W.Nonsingular (W.neg P)$$$

Lean4

theorem addZ_neg (P : Fin 3 → R) : addZ P (W'.neg P) = 0 :=
  addZ_of_X_eq rfl

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

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

Разделы

Аффилиация

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