neg_equiv

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

If P ≈ Q in the projective sense, then W'.neg P ≈ W'.neg Q.

Русский

Если P эквивалентна Q в проективном смысле, то W'.neg P эквивалентна W'.neg Q.

LaTeX

$$$$P \approx Q \implies W'.neg P \approx W'.neg Q$$$$

Lean4

theorem neg_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.neg P ≈ W'.neg Q :=
  by
  rcases h with ⟨u, rfl⟩
  exact neg_smul_equiv Q u.isUnit

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

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

Разделы

Аффилиация

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