singletonMonoidHom — Mathlib

English

The singleton map α → Set α sending a to {a} is a MonoidHom.

Русский

Одноэлементное отображение α → Set α, отправляющее a в {a}, является моноид-гомоморфизмом.

LaTeX

$$$$ singletonMonoidHom: \alpha \to^* Set \alpha \quad \text{is a monoid hom (preserves }1\text{ and }\cdot). $$$$

Lean4

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

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