smulCommClass'' — Mathlib

English

If SMul (β i) (γ i), SMul (α i) (γ i) and SMulCommClass (α i) (β i) (γ i) hold for all i, then SMulCommClass ((i → α i)) ((i → β i)) ((i → γ i)).

Русский

Если для всех i выполняются SMul (β_i)(γ_i), SMul (α_i)(γ_i) и SMulCommClass (α_i)(β_i)(γ_i), то SMulCommClass (∀ i, α_i) (∀ i, β_i) (∀ i, γ_i).

LaTeX

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

Lean4

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

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