Y_eq_of_equiv

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

← MathLib Explorer

English

If P ≈ Q then P y / P z = Q y / Q z when P z ≠ 0 and Q z ≠ 0.

Русский

Если P ≈ Q, то P y / P z = Q y / Q z при P z ≠ 0 и Q z ≠ 0.

LaTeX

$$P(1)/P(2) = Q(1)/Q(2)$$

Lean4

theorem Y_eq_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P y * Q z = Q y * P z :=
  by
  rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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

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

Разделы

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

Аффилиация

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