weightedHomogeneousSubmodule_eq_finsupp_supported

English

The weighted homogeneous submodule equals the finsupp-supported submodule corresponding to the set {d | weight w d = m}. This gives a convenient definitional form.

Русский

Весовой однородный подмодуль равен подмодулю fat над Finsupp, поддерживаемому множеством {d | weight w d = m}.

LaTeX

$$weightedHomogeneousSubmodule R w m = Finsupp.supported R R {d | weight w d = m}$$

Lean4

/-- The submodule `weightedHomogeneousSubmodule R w m` of homogeneous `MvPolynomial`s of
  degree `n` is equal to the `R`-submodule of all `p : (σ →₀ ℕ) →₀ R` such that
  `p.support ⊆ {d | weight w d = m}`. While equal, the former has a
  convenient definitional reduction. -/
theorem weightedHomogeneousSubmodule_eq_finsupp_supported (w : σ → M) (m : M) :
    weightedHomogeneousSubmodule R w m = Finsupp.supported R R {d | weight w d = m} :=
  by
  ext x
  rw [mem_supported, Set.subset_def]
  simp only [Finsupp.mem_support_iff, mem_coe]
  rfl

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