Theorems · Theorem · field theory
MvPolynomial.algebraicIndependent_polynomial_aeval_X
∀ {ι : Type u_1} {R : Type u_3} [inst : CommRing R] (f : ι → Polynomial R),
(∀ (i : ι), Transcendental R (f i)) → AlgebraicIndependent R fun i => (Polynomial.aeval (MvPolynomial.X i)) (f i)If for each i : ι, f_i : R[X] is transcendental over R, then {f_i(X_i) | i : ι}
in MvPolynomial ι R is algebraically independent over R.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setproof · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Set.Elemproof · cited by 7,166
- Polynomialstatement and proof · cited by 5,681
- Set.imageproof · cited by 5,609
- Finsuppstatement · cited by 5,255
- AlgHomstatement · cited by 3,236
- MvPolynomialstatement and proof · cited by 2,140
- Set.Finiteproof · cited by 1,814
- Polynomial.aevalstatement and proof · cited by 615
- MvPolynomial.Xstatement and proof · cited by 552
Cited by1
Results whose statement or proof uses this declaration.
- AlgebraicIndependent.polynomial_aeval_of_transcendentalproof · cited by 0