singletonMonoidHom — Mathlib

English

The map a ↦ {a} defines a Monoid Hom from α to Finset α.

Русский

Отображение a ↦ {a} задает однородную моноид-гомоморфизм (Monoid Hom) из α в Finset α.

LaTeX

$$$$ \\text{singletonMonoidHom: } \\alpha \\to^* Finset\\,\\alpha $$$$

Lean4

/-- The singleton operation as a `MonoidHom`. -/
@[to_additive /-- The singleton operation as an `AddMonoidHom`. -/
    ]
def singletonMonoidHom : α →* Finset α :=
  { singletonMulHom, singletonOneHom with }

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