homogeneousSubmodule_eq_finsupp_supported

English

The product of homogeneous submodules of degrees m and n is contained in the homogeneous submodule of degree m+n.

Русский

Произведение однородных подмодулей степеней m и n содержится в однородном подмодуле степени m+n.

LaTeX

$$$\\text{homogeneousSubmodule}(m,R) \\cdot \\text{homogeneousSubmodule}(n,R) \\leq \\text{homogeneousSubmodule}(m+n,R)$$$

Lean4

/-- While equal, the former has a convenient definitional reduction. -/
theorem homogeneousSubmodule_eq_finsupp_supported (n : ℕ) :
    homogeneousSubmodule σ R n = Finsupp.supported _ R {d | d.degree = n} :=
  by
  simp_rw [degree_eq_weight_one]
  exact weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n

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