negY_of_Z_ne_zero — Mathlib

English

Scaling P by u scales negY by u^3.

Русский

Умножение P на u масштабирует negY в соответствии с степенью 3: negY(uP) = u^3 negY(P).

LaTeX

$$$$ W'.negY(u \\cdot P) = u^3 \\cdot W'.negY(P) $$$$

Lean4

theorem negY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.negY P / P z ^ 3 = W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3) := by
  linear_combination (norm := (rw [negY, Affine.negY]; ring1))
    -W.a₁ * P x / P z ^ 2 * div_self hPz - W.a₃ * div_self (pow_ne_zero 3 hPz)

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