rat'

Mathlib.Algebra.Module.Rat

URI: https://scilib.ai/kg/mathlib#SMulCommClass.rat'

English

There is SMulCommClass rat' asserting commutativity of Rat scalars with ring actions.

Русский

Существует SMulCommClass rat' о взаимном приводе рациональных скаляров и кольцевых действий.

LaTeX

$$$\\text{SMulCommClass } \\mathrm{Rat} \\; \\alpha \\; M$$$

Lean4

instance rat' [Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] : SMulCommClass α ℚ M :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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