singletonMulHom — Mathlib

English

The singleton operation defines a MulHom α → Set α, sending a to {a} and preserving multiplication.

Русский

Операция создания единичного множества определяет мульхомом α → Set α, отображая a в {a} и сохраняющей умножение.

LaTeX

$$singletonMulHom : α →ₙ* Set α with toFun := singleton and map_mul' a b := singleton_mul_singleton.symm$$

Lean4

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

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