coeMonoidHom — Mathlib

English

coeMonoidHom is the MonoidHom sending a Finset to its underlying set, i.e., S ↦ S as a subset of α; it preserves multiplication via set-product.

Русский

coeMonoidHom — моноид-гомоморфизм, переводящий Finset α в Set α через отображение S ↦ S как подмножество α; сохраняет умножение через произведение множеств.

LaTeX

$$$$ \\text{coeMonoidHom: Finset }\\alpha \\to^* Set\\,\\alpha, \\; S \\mapsto S $$$$

Lean4

/-- The coercion from `Finset` to `Set` as a `MonoidHom`. -/
@[to_additive /-- The coercion from `Finset` to `set` as an `AddMonoidHom`. -/
    ]
def coeMonoidHom : Finset α →* Set α where
  toFun := (↑)
  map_one' := coe_one
  map_mul' := coe_mul

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