smulCommClass'

Mathlib.FieldTheory.Fixed

URI: https://scilib.ai/kg/mathlib#FixedPoints.smulCommClass'

English

The symmetric SMulCommClass for FixedPoints.subfield and M acts compatibly with F.

Русский

Симметричное SMulCommClass для FixedPoints.subfield и M действует согласованно с F.

LaTeX

$$$ SMulCommClass (FixedPoints.subfield M F) M F $$$

Lean4

instance smulCommClass' : SMulCommClass (FixedPoints.subfield M F) M F :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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