torsionOf_eq_bot_iff_of_noZeroSMulDivisors

English

Assume a ring R is nontrivial and there are no zero-smul divisors on M. Then for m ∈ M, torsionOf(R,M,m) = ⊥ if and only if m ≠ 0.

Русский

Пусть R ненулевой и на M нет нулеподобных делителей умножения. Тогда для m ∈ M, torsionOf(R,M,m) = ⊥ тогда и только если m ≠ 0.

LaTeX

$$$\operatorname{torsionOf}(R,M,m) = \bot \;\iff\; m \neq 0$ (при условиях [Nontrivial R] [NoZeroSMulDivisors R M])$$

Lean4

@[simp]
theorem torsionOf_eq_bot_iff_of_noZeroSMulDivisors [Nontrivial R] [NoZeroSMulDivisors R M] (m : M) :
    torsionOf R M m = ⊥ ↔ m ≠ 0 :=
  by
  refine ⟨fun h contra => ?_, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => ?_⟩
  · rw [contra, torsionOf_zero] at h
    exact bot_ne_top.symm h
  · rw [mem_torsionOf_iff, smul_eq_zero] at hr
    tauto

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