coe_singletonMonoidHom — Mathlib

English

The function coeMonoidHom coincides with the canonical singleton embedding when viewed as MonoidHom.

Русский

Функция coeMonoidHom совпадает с каноническим вложением единичного множества в виде MonoidHom.

LaTeX

$$$$ (singletonMonoidHom : \\alpha \\to Finset\\,\\alpha) = singleton $$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_singletonMonoidHom : (singletonMonoidHom : α → Finset α) = singleton :=
  rfl

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