polynomial_relation — Mathlib

English

Euler's homogeneous relation holds in projective coordinates: 3 × eval P W'.polynomial equals P x × eval P W'.polynomialX + P y × eval P W'.polynomialY + P z × eval P W'.polynomialZ.

Русский

В проективных координатах выполняется гомогенная связь Эйлера: 3 × eval P W'.polynomial = P x × eval P W'.polynomialX + P y × eval P W'.polynomialY + P z × eval P W'.polynomialZ.

LaTeX

$$$3 \\cdot eval P W'.polynomial = P x \\cdot eval P W'.polynomialX + P y \\cdot eval P W'.polynomialY + P z \\cdot eval P W'.polynomialZ$$$

Lean4

/-- Euler's homogeneous function theorem in projective coordinates. -/
theorem polynomial_relation (P : Fin 3 → R) :
    3 * eval P W'.polynomial =
      P x * eval P W'.polynomialX + P y * eval P W'.polynomialY + P z * eval P W'.polynomialZ :=
  by
  rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
  ring1

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