instSMulCommClassSubtypeMemTorsion'

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Submodule.instSMulCommClassSubtypeMemTorsion'

English

There is an SMulCommClass between S and R on the torsion' subtype, making the scalar actions commute as expected.

Русский

Существует SMulCommClass между S и R на подтипе torsion', что обеспечивает коммутативность действий скаляром.

LaTeX

$$SMulCommClass S R (torsion' R M S).$$

Lean4

instance : SMulCommClass S R (torsion' R M S) :=
  ⟨fun _ _ _ => Subtype.ext <| smul_comm _ _ _⟩

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

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

Разделы

Аффилиация

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