localized₀_bot

Mathlib.Algebra.Module.LocalizedModule.Submodule

URI: https://scilib.ai/kg/mathlib#Submodule.localized₀_bot

← MathLib Explorer

English

The localized₀ of the bottom submodule is the bottom submodule in N.

Русский

Локализация bottom-Submodule равна нулевому подмодулю в N.

LaTeX

$$$\\operatorname{localized}_0(p,f,\\bot) = \\bot.$$$

Lean4

@[simp]
theorem localized₀_bot : (⊥ : Submodule R M).localized₀ p f = ⊥ :=
  by
  rw [← le_bot_iff]
  rintro _ ⟨_, rfl, s, rfl⟩
  simp only [IsLocalizedModule.mk'_zero, mem_bot]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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