isTorsionBySet_iff_is_torsion_by_span

Mathlib.Algebra.Module.Torsion

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

← MathLib Explorer

English

IsTorsionBySet s is equivalent to IsTorsionBySet span s.

Русский

IsTorsionBySet s эквивалентно IsTorsionBySet span s.

LaTeX

$$$IsTorsionBySet\,R\,M\,s \;\iff\; IsTorsionBySet\,R\,M\, (\mathrm{span}\,s)$$$

Lean4

theorem isTorsionBySet_iff_is_torsion_by_span : IsTorsionBySet R M s ↔ IsTorsionBySet R M (Ideal.span s) := by
  simpa only [isTorsionBySet_iff_subset_annihilator] using Ideal.span_le.symm

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

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

Разделы

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

Аффилиация

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