torsionBy_one

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Submodule.torsionBy_one

English

The torsion by the unit 1 is trivial: torsionBy(R, M, 1) = {0}.

Русский

Торион по единице равен нулевому подмножеству: torsionBy(R, M, 1) = {0}.

LaTeX

$$$\mathrm{torsionBy}\,R\,M\,1 = \{0\}$$$

Lean4

@[simp]
theorem torsionBy_one : torsionBy R M 1 = ⊥ :=
  eq_bot_iff.mpr fun _ h => by
    rw [mem_torsionBy_iff, one_smul] at h
    exact h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru