bot_N

Mathlib.RingTheory.Filtration

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

English

The bottom filtration has N-component equal to the bottom submodule: (⊥).N = ⊥.

Русский

У нижней фильтрации компонент N равен нулевому подмодулю: (⊥).N = ⊥.

LaTeX

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

Lean4

@[simp]
theorem bot_N : (⊥ : I.Filtration M).N = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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