Theorems · Theorem · commutative algebra

MvPolynomial.support_optionEquivLeft

∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial (Option σ) R),
  ((MvPolynomial.optionEquivLeft R σ) p).support = Finset.image (fun m => m none) p.support

Defined in

Mathlib.Algebra.MvPolynomial.Equiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiring