smul_coe_torsionBy

Mathlib.Algebra.Module.Torsion

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

English

If x is in the torsionBy submodule, then the scalar a agrees with zero when acting on the underlying module element.

Русский

Если x ∈ torsionBy R M a, то a · (x : M) = 0.

LaTeX

$$a • (x : M) = 0$$

Lean4

@[simp]
theorem smul_coe_torsionBy (x : torsionBy R M a) : a • (x : M) = 0 :=
  x.prop

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

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

Разделы

Аффилиация

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