eval₂_denom_ne_zero

Mathlib.FieldTheory.RatFunc.AsPolynomial

URI: https://scilib.ai/kg/mathlib#RatFunc.eval₂_denom_ne_zero

English

If eval f a x ≠ 0, then Polynomial.eval₂ f a (denom x) ≠ 0.

Русский

Если eval f a x ≠ 0, то Polynomial.eval₂ f a (denom x) ≠ 0.

LaTeX

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

Lean4

theorem eval₂_denom_ne_zero {x : RatFunc K} (h : eval f a x ≠ 0) : Polynomial.eval₂ f a (denom x) ≠ 0 :=
  mt eval_eq_zero_of_eval₂_denom_eq_zero h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru