instQuotientIdealSpanSubmoduleHSMulSetTop

Mathlib.Algebra.Module.Torsion

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

← MathLib Explorer

English

IsTorsionBySet R (M ⧸ I • ⊤) I holds for all I.

Русский

IsTorsionBySet R (M / (I • ⊤)) I верно для всех I.

LaTeX

$$$IsTorsionBySet R (M \\ / (I \\cdot \\top)) I$$$

Lean4

instance : Module (R ⧸ Ideal.span s) (M ⧸ s • (⊤ : Submodule R M)) :=
  ((isTorsionBySet_iff_is_torsion_by_span s).mp (isTorsionBySet_quotient_set_smul M s)).module

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

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

Разделы

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

Аффилиация

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