dblXYZ_of_Y_eq' — Mathlib

English

Another presentation of the Z=0 case: dblXYZ(P) equals P_x^2 times the standard basis vector [1,1,0].

Русский

Другой вариант случая Z=0: dblXYZ(P) = P_x^2 · [1,1,0].

LaTeX

$$$\\mathrm{dblXYZ}(P) = P_x^2 \\cdot [1,1,0]$$$

Lean4

theorem dblXYZ_of_Y_eq' [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 = Q y * P z ^ 3) (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) :
    W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0] := by
  rw [dblXYZ, dblX_of_Y_eq hQz hx hy hy', dblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']

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