Theorems · Definition · commutative algebra

MvPolynomial.homogeneousComponent

{σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → ℕ → MvPolynomial σ R →ₗ[R] MvPolynomial σ R

homogeneousComponent n φ is the part of φ that is homogeneous of degree n. See sum_homogeneousComponent for the statement that φ is equal to the sum of all its homogeneous components.

Defined in

Mathlib.RingTheory.MvPolynomial.Homogeneous

Cited by

17 results in Mathlib

Foundations

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

Assumes

CommSemiring