homogeneousComponent_of_mem — Mathlib

English

If p ∈ homogeneousSubmodule n, then homogeneousComponent m p = p when m = n, and 0 otherwise.

Русский

Если p принадлежит однородному подмодулю степени n, то для любой m: homogeneousComponent(m) p = p если m=n, иначе 0.

LaTeX

$$p ∈ homogeneousSubmodule σ R n ⇒ homogeneousComponent m p = if m = n then p else 0$$

Lean4

theorem homogeneousComponent_of_mem {m n : ℕ} {p : MvPolynomial σ R} (h : p ∈ homogeneousSubmodule σ R n) :
    homogeneousComponent m p = if m = n then p else 0 :=
  weightedHomogeneousComponent_of_mem h

Похожие утверждения