smulCommClass_set' — Mathlib

English

An alternative Smul-commutativity instance for sets: SMulCommClass (Set α) (Set β) (Set γ).

Русский

Альтернативный пример коммутативности умножения для множеств: SMulCommClass (Set α) (Set β) (Set γ).

LaTeX

$$$ SMulCommClass\,(Set\,\alpha) (Set\,\beta) (Set\,\gamma) $$$

Lean4

@[to_additive]
instance smulCommClass_set' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Set β) (Set γ) :=
  ⟨fun _ _ _ ↦ image_image2_distrib_right <| smul_comm _⟩

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