torsionOf_eq_top_iff — Mathlib

English

For a module M and m ∈ M, the torsionOf of m equals the whole ring if and only if m = 0.

Русский

Для m ∈ M тorsionOf(m) равен ⊤ тогда, когда m = 0, и неравен, если m ≠ 0.

LaTeX

$$$\operatorname{torsionOf}(R,M,m) = \top \;\Longleftrightarrow\; m = 0$$$

Lean4

@[simp]
theorem torsionOf_eq_top_iff (m : M) : torsionOf R M m = ⊤ ↔ m = 0 :=
  by
  refine ⟨fun h => ?_, fun h => by simp [h]⟩
  rw [← one_smul R m, ← mem_torsionOf_iff m (1 : R), h]
  exact Submodule.mem_top

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