smulCommClass' — Mathlib

English

If α, Ring, and their actions satisfy the usual compatibilities, then the induced commutativity property also holds when the scalar order is reversed, i.e., SMulCommClass c.Quotient α c.Quotient.

Русский

Если выполняются обычные совместимости между α и RingCon, то свойство коммутации скаляров сохраняется и при изменении очередности действий: SMulCommClass c.Quotient α c.Quotient.

LaTeX

$$$$ \text{SMulCommClass } c^{\Quotient} \ α \ c^{\Quotient} $$$$

Lean4

instance smulCommClass' [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] (c : RingCon R) :
    SMulCommClass c.Quotient α c.Quotient :=
  haveI := SMulCommClass.symm R α R
  SMulCommClass.symm _ _ _

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