torsionBySet_singleton_eq — Mathlib

English

Let R be a commutative semiring and M an R-module. For any a ∈ R, the submodule of torsion elements defined using the singleton {a} coincides with the torsion submodule defined by a: torsionBySet(R, M, {a}) = torsionBy(R, M, a).

Русский

Пусть R — коммутативное полускольное кольцо, M — модуль над R. Для любого a ∈ R подмодуль ториона по одиночному множеству {a} совпадает с торионом по элементу a: torsionBySet(R, M, {a}) = torsionBy(R, M, a).

LaTeX

$$$\mathrm{torsionBySet}\,R\,M\,{\{a\}} = \mathrm{torsionBy}\,R\,M\,a$$$

Lean4

@[simp]
theorem torsionBySet_singleton_eq : torsionBySet R M { a } = torsionBy R M a :=
  by
  ext x
  simp only [mem_torsionBySet_iff, SetCoe.forall, Set.mem_singleton_iff, forall_eq, mem_torsionBy_iff]

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