smulCommClass_right — Mathlib

English

Similarly, the SMul-commutativity holds for X, Y with the right subfield action.

Русский

Аналогично, свойство SMulCommClass выполняется справа для X, Y и подполе.

LaTeX

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

Lean4

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

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