eval_eq_zero_of_eval₂_denom_eq_zero

English

If the denominator evaluates to zero under f and a, then eval f a x equals zero.

Русский

Если знаменатель x при подстановке через f и a даёт ноль, то eval f a x равно нулю.

LaTeX

$$$ \text{Polynomial.eval}_2 f a (\operatorname{denom} x) = 0 \Rightarrow \mathrm{eval} f a x = 0$$$

Lean4

theorem eval_eq_zero_of_eval₂_denom_eq_zero {x : RatFunc K} (h : Polynomial.eval₂ f a (denom x) = 0) : eval f a x = 0 :=
  by rw [eval, h, div_zero]

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