negAddY_smul — Mathlib

English

The negAddY coordinate is homogeneous of degree 2 in the input coordinates: negAddY(u·P, v·Q) = (uv)^2 negAddY(P,Q).

Русский

Y-координата отрицания суммы тоже однородна по степени: negAddY(u·P, v·Q) = (uv)^2 negAddY(P,Q).

LaTeX

$$$W'.negAddY(u\cdot P, v\cdot Q) = (uv)^2 \cdot W'.negAddY(P,Q).$$

Lean4

theorem negAddY_smul (P Q : Fin 3 → R) (u v : R) : W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q :=
  by
  simp only [negAddY, smul_fin3_ext]
  ring1

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