Transcendental elements in MvPolynomial

This file lists some results on some elements in MvPolynomial σ R being transcendental over the base ring R and subrings MvPolynomial.supported of MvPolynomial σ R.

theorem MvPolynomial.transcendental_supported_polynomial_aeval_X {σ : Type u_1} (R : Type u_2) [CommRing R] {i : σ} {s : Set σ} (h : i ∉ s) {f : Polynomial R} (hf : Transcendental R f) : Transcendental (↥(MvPolynomial.supported R s)) ((Polynomial.aeval (MvPolynomial.X i)) f)

theorem MvPolynomial.transcendental_polynomial_aeval_X {σ : Type u_1} (R : Type u_2) [CommRing R] (i : σ) {f : Polynomial R} (hf : Transcendental R f) : Transcendental R ((Polynomial.aeval (MvPolynomial.X i)) f)

theorem MvPolynomial.transcendental_polynomial_aeval_X_iff {σ : Type u_1} (R : Type u_2) [CommRing R] (i : σ) {f : Polynomial R} : Transcendental R ((Polynomial.aeval (MvPolynomial.X i)) f) ↔ Transcendental R f

theorem MvPolynomial.transcendental_supported_polynomial_aeval_X_iff {σ : Type u_1} (R : Type u_2) [CommRing R] [Nontrivial R] {i : σ} {s : Set σ} {f : Polynomial R} : Transcendental (↥(MvPolynomial.supported R s)) ((Polynomial.aeval (MvPolynomial.X i)) f) ↔ i ∉ s ∧ Transcendental R f

theorem MvPolynomial.transcendental_supported_X {σ : Type u_1} (R : Type u_2) [CommRing R] {i : σ} {s : Set σ} (h : i ∉ s) : Transcendental (↥(MvPolynomial.supported R s)) (MvPolynomial.X i)

theorem MvPolynomial.transcendental_X {σ : Type u_1} (R : Type u_2) [CommRing R] (i : σ) : Transcendental R (MvPolynomial.X i)

theorem MvPolynomial.transcendental_supported_X_iff {σ : Type u_1} (R : Type u_2) [CommRing R] [Nontrivial R] {i : σ} {s : Set σ} : Transcendental (↥(MvPolynomial.supported R s)) (MvPolynomial.X i) ↔ i ∉ s