toAffineLift_add — Mathlib

English

Addition preserved by the affine lift: (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift.

Русский

Сохранение сложения через аффинное восхождение: (P+Q).toAffineLift = P.toAffineLift + Q.toAffineLift.

LaTeX

$$$(P+Q).toAffineLift = P.toAffineLift + Q.toAffineLift$$$

Lean4

theorem toAffineLift_add [DecidableEq F] (P Q : W.Point) : (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift :=
  by
  rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩
  exact toAffine_add hP hQ

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