dblU_eq — Mathlib

English

dblU equals the explicit expression: W.dblU P = (W.a1 P_y P_z - (3 P_x^2 + 2 W.a2 P_x P_z + W.a4 P_z^2))^3 / P_z^2.

Русский

dblU равно выражению: W.dblU P = (W.a1 P_y P_z − (3 P_x^2 + 2 W.a2 P_x P_z + W.a4 P_z^2))^3 / P_z^2.

LaTeX

$$$ W.dblU P = \\left( W.a_1 P_y P_z - \\left( 3 P_x^2 + 2 W.a_2 P_x P_z + W.a_4 P_z^2 \\right) \\right)^3 / P_z^2 $$$

Lean4

theorem dblU_eq (P : Fin 3 → F) :
    W.dblU P = (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2 := by
  rw [dblU, eval_polynomialX]

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