Theorems · Theorem · commutative algebra

MvPolynomial.pderiv_inr_universalFactorizationMap_X

∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin k) (j : Fin n),
  (MvPolynomial.pderiv (Sum.inr i))
      ((MvPolynomial.tensorEquivSum R (Fin m) (Fin k) R)
        ((MvPolynomial.universalFactorizationMap R n m k hn) (MvPolynomial.X j))) =
    if ↑j < ↑i then 0
    else if h : ↑j - ↑i < m then MvPolynomial.X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0

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