image_smul_distrib — Mathlib

English

Let f be a structure-preserving map and a ∈ α. The image of a • s under f equals f(a) • s.image(f).

Русский

Пусть f сохраняет структуру, и a ∈ α. Образ a • s равен f(a) • образ(f, s).

LaTeX

$$$(a \\cdot s).image\, f = (f(a)) \\cdot (s.image\, f)$$$

Lean4

@[to_additive]
theorem image_smul_distrib [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F)
    (a : α) (s : Finset α) : (a • s).image f = f a • s.image f :=
  image_comm <| map_mul _ _

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