decompose'_eq — Mathlib

English

The decomposition outside of the above is equal to the explicit equivalence constructed by weightedDecomposition.

Русский

Разложение совпадает с явным равенством, построенным через weightedDecomposition.

LaTeX

$$decomposition.decompose' = (fun φ => DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (φ.support.image Finsupp.degree) (fun m => ⟨homogeneousComponent m φ, homogeneousComponent_mem m φ⟩))$$

Lean4

theorem decompose'_eq :
    decomposition.decompose' = fun φ : MvPolynomial σ R =>
      DirectSum.mk (fun i : ℕ => ↥(homogeneousSubmodule σ R i)) (φ.support.image Finsupp.degree) fun m =>
        ⟨homogeneousComponent m φ, homogeneousComponent_mem m φ⟩ :=
  by
  rw [degree_eq_weight_one]
  rfl

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