stableFiltration_stable

Mathlib.RingTheory.Filtration

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

← MathLib Explorer

English

The stableFiltration satisfies that it is stable by construction.

Русский

Стандартная устойчивая фильтрация устойчива по конструированию.

LaTeX

$$Stable(I.stableFiltration N)$$

Lean4

theorem _root_.Ideal.stableFiltration_stable (I : Ideal R) (N : Submodule R M) : (I.stableFiltration N).Stable :=
  by
  use 0
  intro n _
  dsimp
  rw [add_comm, pow_add, mul_smul, pow_one]

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

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

Разделы

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

Аффилиация

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