image_smul_comm — Mathlib

English

If f respects the smul action, then f''(a • s) = a • f''(s).

Русский

Если отображение f сохраняет действие scm, то образ a • s равен a • образу s.

LaTeX

$$$ (\forall b, f(a \cdot b) = a \cdot f(b)) \Rightarrow f '' (a \cdot s) = a \cdot f '' s $$$

Lean4

@[to_additive]
theorem image_smul_comm [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Set β) :
    (∀ b, f (a • b) = a • f b) → f '' (a • s) = a • f '' s :=
  image_comm

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