toAffineLift_neg — Mathlib

English

Negation commutes with the affine lift: the affine lift of -P equals the negation of the affine lift of P.

Русский

Отрицание коммутирует с аффинным подъемом: аффинная подъемность -P равна отрицанию аффинной подъемности P.

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

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