imageMulHom — Mathlib

English

The image lifting to Finset via imageMulHom preserves multiplication: imageMulHom f acts on Finset α to Finset β by mapping s to image f s.

Русский

Перенос образа в Finset через imageMulHom сохраняет умножение: imageMulHom f переводит Finset α в Finset β, отправляя s в image f s.

LaTeX

$$imageMulHom f : Finset α → Finset β$$

Lean4

/-- Lift a `MulHom` to `Finset` via `image`. -/
@[to_additive (attr := simps) /-- Lift an `AddHom` to `Finset` via `image` -/
    ]
def imageMulHom [DecidableEq β] : Finset α →ₙ* Finset β
    where
  toFun := Finset.image f
  map_mul' _ _ := image_mul _

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