Theorems · Theorem · commutative algebra

MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm

∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {n : ℕ} [hσ : Finite σ] {p : Polynomial (MvPolynomial σ R)},
  ((MvPolynomial.optionEquivLeft R σ).symm p).IsHomogeneous n → ∀ (i j : ℕ), i + j = n → (p.coeff i).IsHomogeneous j

Defined in

Mathlib.RingTheory.MvPolynomial.Homogeneous

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringFinite