aeval — Mathlib

English

If r is transcendental over R and f is a nonzero polynomial with lc ∈ R^0, then aeval r f is transcendental over R.

Русский

Если r трансцендентен над R и f — ненулевой полином с lc ∈ R^0, то aeval r f трансцендентен над R.

LaTeX

$$$ \forall r : A,\ H : Transcendental R r, \forall f : R[X],\ f.natDegree \neq 0 \to f.leadingCoeff \in R^0 \to Transcendental R (aeval r f) $$$

Lean4

theorem aeval {r : A} (H : Transcendental R r) (f : R[X]) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ R⁰) :
    Transcendental R (aeval r f) := fun h ↦ H (h.of_aeval f hf hf')

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