isTorsionBySet_annihilator_top

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Module.isTorsionBySet_annihilator_top

← MathLib Explorer

English

IsTorsionBySet for annihilator of top is torsion.

Русский

IsTorsionBySet для аннигиляторного верха — торсионность.

LaTeX

$$Module.IsTorsionBySet R M (⊤:Submodule R M).annihilator$$

Lean4

theorem _root_.Module.isTorsionBySet_annihilator_top : Module.IsTorsionBySet R M (⊤ : Submodule R M).annihilator :=
  fun x ha => mem_annihilator.mp ha.prop x mem_top

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

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

Разделы

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

Аффилиация

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