Theorems · Definition · commutative algebra

MvPolynomial.optionEquivLeft

(R : Type u) → (S₁ : Type v) → [inst : CommSemiring R] → MvPolynomial (Option S₁) R ≃ₐ[R] Polynomial (MvPolynomial S₁ R)

The algebra isomorphism between multivariable polynomials in Option S₁ and polynomials with coefficients in MvPolynomial S₁ R.

Defined in

Mathlib.Algebra.MvPolynomial.Equiv

Cited by

36 results in Mathlib

Foundations

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

Assumes

CommSemiring