toAffineLift_neg

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

Negation commutes with the affine lift: (-P).toAffineLift = - P.toAffineLift.

Русский

Отрицание commute с восхождением к аффинной точке: (-P).toAffineLift = - P.toAffineLift.

LaTeX

$$$(-P).toAffineLift = -\\,P.toAffineLift$$$

Lean4

theorem toAffineLift_neg (P : W.Point) : (-P).toAffineLift = -P.toAffineLift :=
  by
  rcases P with @⟨⟨_⟩, hP⟩
  exact toAffine_neg hP

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

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

Разделы

Аффилиация

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