Theorems · Definition · field theory
Polynomial.Bivariate.equivMvPolynomial
(R : Type u_1) → [inst : CommSemiring R] → Polynomial (Polynomial R) ≃ₐ[R] MvPolynomial (Fin 2) R
The equiv between R[X][Y] and R[X, Y].
- Defined in
- Mathlib.Algebra.Polynomial.Bivariate
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement · cited by 5,681
- Finsuppstatement · cited by 5,255
- MvPolynomialstatement · cited by 2,140
- AlgEquivstatement · cited by 1,681
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- Matrix.vecConsproof · cited by 852
- Matrix.vecEmptyproof · cited by 832
- MvPolynomial.Xproof · cited by 552
- MvPolynomial.aevalproof · cited by 298
Cited by15
Results whose statement or proof uses this declaration.
- StandardEtalePresentation.toPresentationproof · cited by 5
- Polynomial.Bivariate.equivMvPolynomial_Xstatement · cited by 3
- Polynomial.Bivariate.equivMvPolynomial_C_Xstatement · cited by 3
- StandardEtalePair.equivMvPolynomialQuotientstatement and proof · cited by 3
- Polynomial.Bivariate.equivMvPolynomial_C_Cstatement · cited by 2
- StandardEtalePresentation.aeval_val_equivMvPolynomialstatement and proof · cited by 1
- StandardEtalePresentation.toPresentation_relationstatement and proof · cited by 1
- StandardEtalePresentation.toPresentation_valstatement · cited by 1
- Polynomial.Bivariate.equivMvPolynomial_symm_X_0statement · cited by 1
- Polynomial.Bivariate.pderiv_one_equivMvPolynomialstatement and proof · cited by 1
- Polynomial.Bivariate.pderiv_zero_equivMvPolynomialstatement and proof · cited by 1
- StandardEtalePair.equivMvPolynomialQuotient_symm_applystatement · cited by 1