instSMulCommClassSubtypeMemSubfieldSubfield

English

SMul commutes between M-actions on FixedPoints.subfield and F under suitable structure.

Русский

Свойство коммутирования умножения между действиями M на FixedPoints.subfield и на F при подходящей структуре.

LaTeX

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

Lean4

instance : SMulCommClass M (FixedPoints.subfield M F) F where
  smul_comm m f f' := show m • (↑f * f') = f * m • f' by rw [smul_mul', f.prop m]

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