X_eq_iff

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

English

If P z ≠ 0 and Q z ≠ 0, then P x × Q z = Q x × P z if and only if P x / P z = Q x / Q z.

Русский

Если P z ≠ 0 и Q z ≠ 0, то P x Q z = Q x P z эквивалентно P x / P z = Q x / Q z.

LaTeX

$$(P x)(Q z) = (Q x)(P z) \iff P x / P z = Q x / Q z$$

Lean4

theorem X_eq_iff {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) : P x * Q z = Q x * P z ↔ P x / P z = Q x / Q z :=
  (div_eq_div_iff hPz hQz).symm

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

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

Разделы

Аффилиация

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