dualAnnihilator_bot

Mathlib.LinearAlgebra.Dual.Defs

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

English

The dual annihilator of the bottom submodule is the top submodule.

Русский

Дуальный аннигилирующий подмодуля ноль даёт верхний подмодуль.

LaTeX

$$(⊥).dualAnnihilator = ⊤$$

Lean4

@[simp]
theorem dualAnnihilator_bot : (⊥ : Submodule R M).dualAnnihilator = ⊤ :=
  (dualAnnihilator_gc R M).l_bot

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

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

Разделы

Аффилиация

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