toStarMonoidHom — Mathlib

English

Reinterpret a StarMulEquiv as a StarMonoidHom: for e ∈ A ≃⋆* B, define a StarMonoidHom whose toFun is e, and whose preservation of identity, multiplication, and star holds.

Русский

Преобразовать StarMulEquiv в StarMonoidHom: для e ∈ A ≃⋆* B задано звездное моноидное отображение, у которого toFun равно e и сохраняются единица, умножение и операция звезды.

LaTeX

$$$(\\operatorname{toStarMonoidHom}(e))(a) = e(a) \\quad \\text{for all } a \\in A$$$

Lean4

/-- Reinterpret a `StarMulEquiv` as a `StarMonoidHom`. -/
@[simps]
def toStarMonoidHom (f : A ≃⋆* B) : A →⋆* B where
  toFun := f
  map_one' := map_one f
  map_mul' := map_mul f
  map_star' := map_star f

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