Y_eq_iff'

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.Y_eq_iff'

← MathLib Explorer

English

A variant of Y equality: under similar hypotheses, P_y Q_z = negY Q P_z.

Русский

Вариант Y-равенства: при сходных гипотезах P_y Q_z = negY Q P_z.

LaTeX

$$$ P_y Q_z = W'.negY Q P_z $$$

Lean4

theorem Y_eq_iff' {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
    P y * Q z = W.negY Q * P z ↔ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z) :=
  negY_of_Z_ne_zero hQz ▸ (div_eq_div_iff hPz hQz).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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