smulCommClass' — Mathlib

English

If each SMul structure on β i, α i, and SMulCommClass holds pointwise, then SMulCommClass M (∀ i, α i) (∀ i, β i).

Русский

Если на β_i и α_i выполняются соответствующие SMul структуры и SMulCommClass покоординатно, то SMulCommClass на (∀ i, α i) и (∀ i, β i).

LaTeX

$$$\text{SMulCommClass } M (∀ i, α i) (∀ i, β i)$$$

Lean4

@[to_additive]
instance smulCommClass' [∀ i, SMul M (β i)] [∀ i, SMul (α i) (β i)] [∀ i, SMulCommClass M (α i) (β i)] :
    SMulCommClass M (∀ i, α i) (∀ i, β i) :=
  ⟨fun x y z => funext fun i ↦ smul_comm x (y i) (z i)⟩

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