singletonMulHom — Mathlib

English

There is a natural MulHom sending x to the singleton {x}, i.e., the singleton construction acts as a multiplicative homomorphism from α to Finset α.

Русский

Существует естественный MulHom, переводящий x в одноэлементное множество {x}, то есть отображение singleton является мультипликативным гомомом.

LaTeX

$$Finset.singletonMulHom : α → Finset α$$

Lean4

/-- The singleton operation as a `MulHom`. -/
@[to_additive /-- The singleton operation as an `AddHom`. -/
    ]
def singletonMulHom : α →ₙ* Finset α where toFun := singleton; map_mul' _ _ := (singleton_mul_singleton _ _).symm

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