Theorems · Theorem · commutative algebra

MvPolynomial.uniqueAlgEquiv_symm_monomial

∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Unique σ] {d : σ →₀ ℕ} {r : R},
  (MvPolynomial.uniqueAlgEquiv R σ).symm ((Polynomial.monomial (d default)) r) = (MvPolynomial.monomial d) r

Defined in

Mathlib.Algebra.MvPolynomial.Equiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringUnique