image_smul_comm — Mathlib

English

If f is a function that commutes with smul, then the image under f of the scalar multiple of a Finset s equals the scalar multiple of the image of s: (a • s).image f = a • s.image f.

Русский

Если f сохраняет совместимость со скаляром, то образ под действием f от скалярного умножения множества равен скалярному умножению образа множества: (a • s).image f = a • (s.image f).

LaTeX

$$$\\forall f\\, a\\, s, (\\forall b, f(a • b) = a • f b) \\Rightarrow \\mathrm{image}\, f (a • s) = a • \\mathrm{image}\, f s$$$

Lean4

@[to_additive]
theorem image_smul_comm [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Finset β) :
    (∀ b, f (a • b) = a • f b) → (a • s).image f = a • s.image f :=
  image_comm

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