transcendental_polynomial_aeval_X_iff

English

For i and f ∈ R[X], Transcendental R (Polynomial.aeval (X i) f) iff Transcendental R f.

Русский

Для i и f ∈ R[X], трансцендентность R (Polynomial.aeval (X_i) f) равна трансцендентности R f.

LaTeX

$$$$\text{Transcendental } R (Polynomial.aeval (X_i : MvPolynomial σ R) f) \iff \text{Transcendental } R f.$$$$

Lean4

theorem transcendental_polynomial_aeval_X_iff (i : σ) {f : R[X]} :
    Transcendental R (Polynomial.aeval (X i : MvPolynomial σ R) f) ↔ Transcendental R f :=
  by
  refine ⟨?_, transcendental_polynomial_aeval_X R i⟩
  simp_rw [Transcendental, not_imp_not]
  exact fun h ↦ h.algHom _

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