isTorsionBy_iff_torsionBy_eq_top — Mathlib

English

An element a gives an a-torsion module iff its torsion submodule is the whole space.

Русский

Элемент a задаёт mоду́ль с торионом по a тогда и только тогда, когда торион по a равен всей пространству.

LaTeX

$$$IsTorsionBy\,R\,M\,a \;\iff\; torsionBy\,R\,M\,a = \top$$$

Lean4

/-- An `a`-torsion module is a module whose `a`-torsion submodule is the full space. -/
theorem isTorsionBy_iff_torsionBy_eq_top : IsTorsionBy R M a ↔ torsionBy R M a = ⊤ := by
  rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff, isTorsionBySet_iff_torsionBySet_eq_top]

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