Theorems · Theorem · commutative algebra

MvPolynomial.universalFactorizationMap_freeMonic

∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  Polynomial.map (↑(MvPolynomial.universalFactorizationMap R n m k hn)) (Polynomial.freeMonic R n) =
    Polynomial.map
        (algebraMap (MvPolynomial (Fin m) R) (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)))
        (Polynomial.freeMonic R m) *
      Polynomial.map (↑Algebra.TensorProduct.includeRight) (Polynomial.freeMonic R k)

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing