Theorems · Theorem · commutative algebra

MvPolynomial.IsHomogeneous.prod

∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ι → MvPolynomial σ R)
  (n : ι → ℕ), (∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)

Defined in

Mathlib.RingTheory.MvPolynomial.Homogeneous

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiring