isSMulRegular_iff_torsionBy_eq_bot

English

For a ring R and a module M, the map defined by multiplying by r is injective if and only if the r-torsion submodule is {0}.

Русский

Пусть R — кольцо, M — модуль. Отображение m ↦ r·m инъективно тогда и только тогда, когда r-торсионный подмодуль равен {0}.

LaTeX

$$IsSMulRegular(M,r) ⇔ torsionBy(R,M,r) = ⊥$$

Lean4

theorem isSMulRegular_iff_torsionBy_eq_bot {R} (M : Type*) [CommRing R] [AddCommGroup M] [Module R M] (r : R) :
    IsSMulRegular M r ↔ Submodule.torsionBy R M r = ⊥ :=
  Iff.symm (DistribMulAction.toLinearMap R M r).ker_eq_bot

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