instTop

Mathlib.RingTheory.Filtration

URI: https://scilib.ai/kg/mathlib#Ideal.Filtration.instTop

English

The top filtration is given by the trivial filtration at the top element, i.e., (⊤ : I.Filtration M).N = ⊤.

Русский

Верхняя фильтрация задаётся тривиальной фильтрацией на верхнем элементе: (⊤).N = ⊤.

LaTeX

$$(⊤ : I.Filtration M).N = ⊤$$

Lean4

instance : Top (I.Filtration M) :=
  ⟨I.trivialFiltration ⊤⟩

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

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

Разделы

Аффилиация

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