dblXYZ_of_Z_eq_zero — Mathlib

English

If the Z-coordinate of the input is zero on a NoZeroDivisors ring, then the doubling vector is supported entirely on the Y-axis: dblXYZ(P) = Py^4 • [0,1,0].

Русский

Если Z координата P равна нулю в кольце без нулей-дивизоров, то вектор удвоения поддержан только по оси Y: dblXYZ(P) = P_y^4 • [0,1,0].

LaTeX

$$$[NoZeroDivisors\ R] \Rightarrow W'.dblXYZ(P) = P_y^4 \cdot \begin{bmatrix}0\\1\\0\end{bmatrix}$$$

Lean4

theorem dblXYZ_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblXYZ P = P y ^ 4 • ![0, 1, 0] := by
  erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3, mul_zero, mul_one]

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