instSMulCommClass — Mathlib

English

Scalar multiplications commute: for all c, f, we have c • f = f • c when appropriate, ensuring commutativity of scalar actions.

Русский

Скалярные умножения коммутируют: для всех c, f верно c • f = f • c (при нужной структуре).

LaTeX

$$$ c \\cdot f = f \\cdot c $$$

Lean4

instance instSMulCommClass [SMulCommClass 𝕜 𝕜' F] : SMulCommClass 𝕜 𝕜' 𝓢(E, F) :=
  ⟨fun a b f => ext fun x => smul_comm a b (f x)⟩

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