English
Euler's homogeneous function relation holds for the Jacobian coordinates: 6 times the polynomial eval equals twice X-eval times X, plus thrice Y-eval times Y, plus Z-coefficient times Z-eval.
Русский
В рамках Якобиана выполняется гомогенная функция Эйлера: 6 умножение на полином равно 2 умноженному на X-eval на eval X, плюс 3 умноженному на Y-eval на eval Y, плюс Z-часть на eval Z.
LaTeX
$$$6 \\cdot \\mathrm{eval} P\,W'.polynomial = 2 \\cdot P x \\cdot \\mathrm{eval} P\,W'.polynomialX + 3 \\cdot P y \\cdot \\mathrm{eval} P\,W'.polynomialY + P z \\cdot \\mathrm{eval} P\,W'.polynomialZ$$$
Lean4
/-- Euler's homogeneous function theorem in Jacobian coordinates. -/
theorem polynomial_relation (P : Fin 3 → R) :
6 * eval P W'.polynomial =
2 * P x * eval P W'.polynomialX + 3 * P y * eval P W'.polynomialY + P z * eval P W'.polynomialZ :=
by
rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
ring1
