Theorems · Theorem · commutative algebra

MvPolynomial.optionEquivLeft_apply

∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (a : MvPolynomial (Option S₁) R),
  (MvPolynomial.optionEquivLeft R S₁) a =
    (MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s)) a

Defined in

Mathlib.Algebra.MvPolynomial.Equiv

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiring