instModuleQuotientAddSubgroupTorsion

English

Given a ring R and an R-module M, the quotient M/torsion M inherits a module structure over R.

Русский

Для кольца R и модуля M модульный фактор по torsion M наследует структуру модуля над R.

LaTeX

$$$\forall (R M : Type*)[Ring R][AddCommGroup M][Module R M],\; Module R (M / AddCommGroup.torsion M)$$$

Lean4

instance {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] : Module R (M ⧸ AddCommGroup.torsion M) :=
  letI : Submodule R M :=
    { AddCommGroup.torsion M with
      smul_mem' := fun r m ⟨n, hn, hn'⟩ ↦
        ⟨n, hn, by {
          simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero, smul_comm n] at hn' ⊢;
          simp only [hn', smul_zero]
        }⟩ }
  inferInstanceAs (Module R (M ⧸ this))

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