image_mul — Mathlib

English

For a map f that respects multiplication, the image of the product equals the product of the images: image f (s * t) = image f s * image f t.

Русский

Для отображения f, сохраняющего умножение, образ произведения равен произведению образов: image f (s * t) = image f s * image f t.

LaTeX

$$Eq (Finset.image f (instHMul.hMul s t)) (instHMul.hMul (Finset.image f s) (Finset.image f t))$$

Lean4

@[to_additive]
theorem image_mul [DecidableEq β] : (s * t).image (f : α → β) = s.image f * t.image f :=
  image_image₂_distrib <| map_mul f

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