mk_int — Mathlib

English

A natural inequality relating powers and smuls in a filtration setting: I^i • F^Nj ≤ F^N(i+j).

Русский

Неравенство в фильтрации: умножение на $I^i$ и слой $F^N j$ не превосходит $F^N (i+j)$.

LaTeX

$$I ^ i • F.N j ≤ F.N (i + j)$$

Lean4

/-- A convenience constructor for `IsModuleFiltration` when the index is the integers. -/
theorem mk_int (F : ℤ → σ) (mono : Monotone F) [SetLike.GradedMonoid F] (F' : ℤ → σM) (mono' : Monotone F')
    [SetLike.GradedSMul F F'] :
    letI := IsRingFiltration.mk_int F mono
    IsModuleFiltration F (fun n ↦ F (n - 1)) F' (fun n ↦ F' (n - 1)) :=
  letI := IsRingFiltration.mk_int F mono
  { IsFiltration.mk_int F' mono' with }

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