isUnit_addZ_of_X_ne

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

English

If addZ P Q ≠ 0 then addZ P Q is a unit.

Русский

Если addZ P Q ≠ 0, то addZ P Q является единицей (обратимым).

LaTeX

$$(addZ P Q) is a unit$$

Lean4

theorem isUnit_addZ_of_X_ne {P Q : Fin 3 → F} (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) : IsUnit <| addZ P Q :=
  (addZ_ne_zero_of_X_ne hx).isUnit

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

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

Разделы

Аффилиация

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