annihilator_bot

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Submodule.annihilator_bot

English

The annihilator equals the top iff the submodule is the bottom (subsingleton) module.

Русский

Аннигилятор равен верхнему вектору тогда, когда подмодуль равен нулю (синглтон).

LaTeX

$$$ N.annihilator = \\top \\iff N = \\bot. $$$

Lean4

theorem annihilator_bot : (⊥ : Submodule R M).annihilator = ⊤ :=
  top_le_iff.mp fun _ _ ↦ mem_annihilator.mpr fun _ ↦ by rintro rfl; rw [smul_zero]

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

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

Разделы

Аффилиация

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