unitsSMulCommClass' — Mathlib

English

Under suitable scalar-scalar interactions, ConjAct units interact properly with scalars, yielding a SMulCommClass.

Русский

При корректном взаимодействии скаляров и единиц, ConjAct образует SMulCommClass.

LaTeX

$$$\text{SMulCommClass }\alpha (ConjAct (Units M)) \; \alpha M$$$

Lean4

instance unitsSMulCommClass' [SMul α M] [SMulCommClass M α M] [IsScalarTower α M M] : SMulCommClass (ConjAct Mˣ) α M :=
  haveI : SMulCommClass α M M := SMulCommClass.symm _ _ _
  SMulCommClass.symm _ _ _

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