smulCommClass_left — Mathlib

English

If F is a subfield of K, then the SMul-commutativity between F, X, and Y holds when X and Y are modules; i.e., the left action of F commutes appropriately with X and Y.

Русский

Если F ⊆ K, то свойство SMulCommClass слева выполняется для X и Y, которые являются модулей над K.

LaTeX

$$$ [SMul K Y] [SMul X Y] [SMulCommClass K X Y] (F : Subfield K) : SMulCommClass F X Y$$

Lean4

instance smulCommClass_left [SMul K Y] [SMul X Y] [SMulCommClass K X Y] (F : Subfield K) : SMulCommClass F X Y :=
  inferInstanceAs (SMulCommClass F.toSubsemiring X Y)

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