Theorems · Definition · commutative algebra
MvPolynomial.sumAlgEquiv
(R : Type u) →
(S₁ : Type v) →
(S₂ : Type w) → [inst : CommSemiring R] → MvPolynomial (S₁ ⊕ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R)The algebra isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.
- Defined in
- Mathlib.Algebra.MvPolynomial.Equiv
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 90 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Finsuppstatement · cited by 5,255
- MvPolynomialstatement · cited by 2,140
- AlgEquivstatement · cited by 1,681
- AlgEquiv.transproof · cited by 108
- Finsupp.sumFinsuppAddEquivProdFinsuppproof · cited by 29
- AddMonoidAlgebra.domCongrproof · cited by 21
- AddMonoidAlgebra.curryAlgEquivproof · cited by 13
Cited by18
Results whose statement or proof uses this declaration.
- MvPolynomial.tensorEquivSumproof · cited by 13
- AlgebraicIndependent.sumElim_iffproof · cited by 2
- MvPolynomial.sumAlgEquiv_X_inlstatement and proof · cited by 2
- MvPolynomial.sumAlgEquiv_X_inrstatement and proof · cited by 2
- Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomialproof · cited by 1
- MvPolynomial.pderiv_sumAlgEquivstatement · cited by 1
- MvPolynomial.sumAlgEquiv_symm_C_Cstatement and proof · cited by 1
- MvPolynomial.sumAlgEquiv_symm_C_Xstatement and proof · cited by 1
- MvPolynomial.sumAlgEquiv_symm_Xstatement and proof · cited by 1
- MvPolynomial.prime_rename_iffproof · cited by 0
- MvPolynomial.coeff_sumAlgEquiv_apply_supportstatement and proof · cited by 0
- MvPolynomial.coeff_sumAlgEquiv_symm_applystatement and proof · cited by 0