smulCommClass_left — Mathlib

English

The scalar actions of the intermediate field are compatible with the action on X from the left, establishing SMulCommClass with left components.

Русский

Действия умножения скалярами промежуточного поля совместимы с левой областью действия на X, образуя SMulCommClass слева.

LaTeX

$$$\\text{SMulCommClass } F X Y$ for $F = S$ (as a subfield)$$

Lean4

instance smulCommClass_left [SMul L Y] [SMul X Y] [SMulCommClass L X Y] (F : IntermediateField K L) :
    SMulCommClass F X Y :=
  inferInstanceAs (SMulCommClass F.toSubfield X Y)

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