smulCommClassBoth — Mathlib

English

The product carries a SMulCommClass when each coordinate does, i.e., SMulCommClass M N (α × β).

Русский

Произведение имеет SMulCommClass, если каждое слагаемое это имеет.

LaTeX

$$$SMulCommClass\\ M\\ N (α × β)$$$

Lean4

@[to_additive]
instance smulCommClassBoth [Mul N] [Mul P] [SMul M N] [SMul M P] [SMulCommClass M N N] [SMulCommClass M P P] :
    SMulCommClass M (N × P) (N × P) where smul_comm c x y := by simp [smul_def, mul_def, mul_smul_comm]

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