quotientAnnihilator — Mathlib

English

There is a natural module structure on M over the ring R/Ann_R(M).

Русский

Существует естественная структура модуля на M над кольцом R/Ann_R(M).

LaTeX

$$$Module\\; (R \\ slash \\ Module.annihilator R M)\\ M$$$

Lean4

/-- Any module is also a module over the quotient of the ring by the annihilator.
Not an instance because it causes synthesis failures / timeouts. -/
def quotientAnnihilator : Module (R ⧸ Module.annihilator R M) M :=
  (isTorsionBySet_annihilator R M).module

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