Theorems · Definition · commutative algebra

MvPolynomial.universalFactorizationMap

(R : Type u_1) →
  [inst : CommRing R] →
    (n m k : ℕ) →
      n = m + k → MvPolynomial (Fin n) R →ₐ[R] TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)

In light of the fact that MonicDegreeEq · n is representable by R[X₁,...,Xₙ], this is the map R[X₁,...,Xₘ₊ₖ] → R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₖ] corresponding to the multiplication MonicDegreeEq · m × MonicDegreeEq · k → MonicDegreeEq · (m + k).

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

19 results in Mathlib

Foundations

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

Assumes

CommRing