stableFiltration

Mathlib.RingTheory.Filtration

URI: https://scilib.ai/kg/mathlib#Ideal.stableFiltration

← MathLib Explorer

English

Definition of stableFiltration: N i := I^i · N.

Русский

Определение stableFiltration: N_i := I^i · N.

LaTeX

$$N_i := I^i • N$$

Lean4

/-- The trivial stable `I`-filtration of `N`. -/
@[simps]
def _root_.Ideal.stableFiltration (I : Ideal R) (N : Submodule R M) : I.Filtration M
    where
  N i := I ^ i • N
  mono i := by rw [add_comm, pow_add, mul_smul]; exact Submodule.smul_le_right
  smul_le i := by rw [add_comm, pow_add, mul_smul, pow_one]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru