Theorems · Definition · commutative algebra
MvPolynomial.sumRingEquiv
(R : Type u) →
(S₁ : Type v) →
(S₂ : Type w) → [inst : CommSemiring R] → MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)The ring 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
- 8 results in Mathlib
- Foundations
- Depth 88 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
- RingEquivstatement · cited by 1,147
- RingEquiv.transproof · cited by 54
- Finsupp.sumFinsuppAddEquivProdFinsuppproof · cited by 29
- AddMonoidAlgebra.mapDomainRingEquivproof · cited by 8
- AddMonoidAlgebra.curryRingEquivproof · cited by 6
Cited by8
Results whose statement or proof uses this declaration.
- MvPolynomial.pderiv_sumRingEquivstatement and proof · cited by 2
- MvPolynomial.sumRingEquiv_Cstatement · cited by 1
- MvPolynomial.sumRingEquiv_X_inlstatement · cited by 1
- MvPolynomial.sumRingEquiv_X_inrstatement · cited by 1
- MvPolynomial.sumRingEquiv_symm_C_Xstatement and proof · cited by 0
- MvPolynomial.sumRingEquiv_symm_Xstatement and proof · cited by 0
- MvPolynomial.pderiv_sumToIterstatement · cited by 0
- MvPolynomial.sumRingEquiv_symm_C_Cstatement and proof · cited by 0