module — Mathlib

English

An (R / Ann_R(M))–module structure exists on M, induced from the given R-module structure on M.

Русский

Существует структура модуля над R/Ann_R(M) на M, индуцированная из данной структуры R-модуля.

LaTeX

$$$\\text{Module } (R \\ / \\ \\operatorname{ann}_R M) \\ M$$$

Lean4

/-- An `(R ⧸ Ideal.span {r})`-module is an `R`-module for which `IsTorsionBy R M r`. -/
abbrev module [h : (Ideal.span { r }).IsTwoSided] (hM : IsTorsionBy R M r) : Module (R ⧸ Ideal.span { r }) M := by
  rw [Ideal.span] at h; exact ((isTorsionBySet_span_singleton_iff r).mpr hM).module

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