mk_int — Mathlib

English

A convenience constructor for IsRingFiltration when the index is the integers: F(n) = F(n-1) and the graded structure is compatible.

Русский

Удобный конструктор IsRingFiltration при индексе целые числа: F(n) = F(n-1) при сохранении градационной структуры.

LaTeX

$$$\\text{IsRingFiltration.mk_int}(F,\\,\\text{mono}) : \\text{IsRingFiltration } F (n \\mapsto F(n-1))$$$

Lean4

/-- A convenience constructor for `IsRingFiltration` when the index is the integers. -/
theorem mk_int (F : ℤ → σ) (mono : Monotone F) [SetLike.GradedMonoid F] : IsRingFiltration F (fun n ↦ F (n - 1)) where
  __ := IsFiltration.mk_int F mono

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