annihilator_span_singleton

Mathlib.RingTheory.Ideal.Maps

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

English

The statement reiterates that N.annihilator = ⊤ iff N = ⊥, aligning with the previous Submodule lemma.

Русский

Утверждение повторяет, что N.annihilator = ⊤ тогда и только тогда, когда N = ⊥.

LaTeX

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

Lean4

theorem annihilator_span_singleton (g : M) : (Submodule.span R { g }).annihilator = ker (toSpanSingleton R M g) := by
  simp [annihilator_span]

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

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

Разделы

Аффилиация

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