trivialFiltration — Mathlib

English

The trivial I-filtration of a submodule N assigns N at every level: F.N(i) = N for all i.

Русский

Тривиальная I-фильтрация подмодуля N задаёт N на каждом уровне: F.N(i) = N для всех i.

LaTeX

$$$F.N(i) = N \quad \text{for all } i$$

Lean4

/-- The trivial `I`-filtration of `N`. -/
@[simps]
def _root_.Ideal.trivialFiltration (I : Ideal R) (N : Submodule R M) : I.Filtration M
    where
  N _ := N
  mono _ := le_rfl
  smul_le _ := Submodule.smul_le_right

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