weightedHomogeneousSubmodule_one — Mathlib

English

The weighted homogeneous submodule with weight 1 at degree n coincides with the standard homogeneous submodule of degree n.

Русский

Взвешенный однородный подмодуль с весом 1 на степень n совпадает с обычным однородным подмодулем степени n.

LaTeX

$$$\\text{weightedHomogeneousSubmodule}_R(1,n) = \\text{homogeneousSubmodule}_{\\sigma} (R,n)$$$

Lean4

@[simp]
theorem weightedHomogeneousSubmodule_one (n : ℕ) : weightedHomogeneousSubmodule R 1 n = homogeneousSubmodule σ R n :=
  rfl

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