Theorems · Theorem · commutative algebra

MvPolynomial.sumAlgEquiv_symm_C_C

∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (r : R),
  (MvPolynomial.sumAlgEquiv R S₁ S₂).symm (MvPolynomial.C (MvPolynomial.C r)) = MvPolynomial.C r

Defined in

Mathlib.Algebra.MvPolynomial.Equiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiring