English
For all i and f ∈ R[X], Transcendental R (Polynomial.aeval (X i : MvPolynomial σ R) f) holds iff Transcendental R f holds.
Русский
Для всех i и f ∈ R[X], трансцендентность R (Polynomial.aeval (X_i) f) эквивалентна трансцендентности R f.
LaTeX
$$$$ \text{Transcendental } R (Polynomial.aeval(X_i : MvPolynomial \sigma R) f) \iff \text{Transcendental } R f. $$$$
Lean4
theorem transcendental_polynomial_aeval_X (i : σ) {f : R[X]} (hf : Transcendental R f) :
Transcendental R (Polynomial.aeval (X i : MvPolynomial σ R) f) :=
by
have := transcendental_supported_polynomial_aeval_X R (Set.notMem_empty i) hf
let g :=
(Algebra.botEquivOfInjective (MvPolynomial.C_injective σ R)).symm.trans
(Subalgebra.equivOfEq _ _ supported_empty).symm
rwa [Transcendental, ←
isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R)) Function.injective_id (by ext1; rfl),
RingHom.id_apply, ← Transcendental]
