annihilator_eq_top_iff

Mathlib.RingTheory.Ideal.Maps

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

English

If N ≤ P, then P.annihilator ≤ N.annihilator.

Русский

Если N ⊆ P, то P.annihilator ⊆ N.annihilator.

LaTeX

$$$ N \\le P \\Rightarrow P.annihilator \\le N.annihilator. $$$

Lean4

theorem annihilator_eq_top_iff : N.annihilator = ⊤ ↔ N = ⊥ := by
  rw [annihilator, Module.annihilator_eq_top_iff, Submodule.subsingleton_iff_eq_bot]

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

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

Разделы

Аффилиация

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