smulCommClass_left — Mathlib

English

Given a subsemiring S of R', if SMul R' β and SMul α β with SMulCommClass R' α β hold, then SMulCommClass S α β also holds.

Русский

Если выполняются условия SMul для R', β и α, β и S ⊆ R', то SMulCommClass для S также выполняется.

LaTeX

$$SMulCommClass S α β$$

Lean4

instance smulCommClass_left [SMul R' β] [SMul α β] [SMulCommClass R' α β] (S : Subsemiring R') : SMulCommClass S α β :=
  inferInstance

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