evalEval_polynomialY_zero — Mathlib

English

Evaluating at (0,0) yields the constant term (up to sign) of W.polynomialY, giving W.a3 at zero.

Русский

Значение в (0,0) даёт константный член полинома W.polynomialY (с учетом знака), равный W.a3 в нуле.

LaTeX

$$evalEval_polynomial_zero : W.polynomialY.evalEval 0 0 = W.a₃$$

Lean4

@[simp]
theorem evalEval_polynomialY_zero : W.polynomialY.evalEval 0 0 = W.a₃ := by
  simp only [evalEval_polynomialY, zero_add, mul_zero]

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