Theorems · Definition · commutative algebra

MvPolynomial.tensorEquivSum

(R : Type u) →
  [inst : CommSemiring R] →
    (σ : Type u_1) →
      (ι : Type u_2) →
        (S : Type u_3) →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] → TensorProduct R (MvPolynomial σ S) (MvPolynomial ι R) ≃ₐ[S] MvPolynomial (σ ⊕ ι) S

S[X] ⊗[R] R[Y] ≃ S[X, Y]

Defined in

Mathlib.RingTheory.TensorProduct.MvPolynomial

Cited by

13 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebra