isTorsionBySet_annihilator — Mathlib

English

The annihilator of M is a set of scalars that annihilate every element of M; thus IsTorsionBySet R M (annihilator R M) holds.

Русский

Аннигилятор M — множество скаляров, уничтожающих каждый элемент M; поэтому IsTorsionBySet(R,M, ann(M)) выполняется.

LaTeX

$$IsTorsionBySet(R,M, annihilator(R,M))$$

Lean4

theorem isTorsionBySet_annihilator : IsTorsionBySet R M (annihilator R M) := fun _ r ↦ Module.mem_annihilator.mp r.2 _

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