map_negY — Mathlib

English

Under the same hypotheses as the previous item but with a different presentation, addXYZ(P,Q) equals addZ(P,Q) times the vector with affine coordinates in the first two entries and 1 in the last entry.

Русский

При тех же гипотезах, но в другой форме, addXYZ(P,Q) = addZ(P,Q) · [X_affine, Y_affine, 1].

LaTeX

$$$\mathrm{addXYZ}(P,Q) = \mathrm{addZ}(P,Q) \cdot \Big(\begin{bmatrix} \mathrm{toAffine.addX}(...) \\ \mathrm{toAffine.addY}(...) \\ 1 \end{bmatrix}\Big)$$$

Lean4

@[simp]
theorem map_negY : (W'.map f).toProjective.negY (f ∘ P) = f (W'.negY P) :=
  by
  simp only [negY]
  map_simp

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