annihilator — Mathlib

English

The annihilator of a submodule is defined as the annihilator of the submodule regarded as an R-module.

Русский

Аннигилятор подмодуля определяется как аннигилятор самого подмодуля, если рассматривать его как R-модуль.

LaTeX

$$$ (N : Submodule R M).annihilator = \\operatorname{Ann}_R(N). $$$

Lean4

/-- `N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`. -/
abbrev annihilator (N : Submodule R M) : Ideal R :=
  Module.annihilator R N

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