colon_bot

Mathlib.RingTheory.Ideal.Colon

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

English

For any N, the colon with bottom equals the annihilator of N: ⊥ col N = Ann(N).

Русский

Для любого N: ⊥ col N = Ann(N).

LaTeX

$$⊥ col N = N.annihilator$$

Lean4

@[simp]
theorem colon_bot : colon ⊥ N = N.annihilator := by
  simp_rw [SetLike.ext_iff, mem_colon, mem_annihilator, mem_bot, forall_const]

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

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

Разделы

Аффилиация

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