copy — Mathlib

English

A copy constructor for a StarMonoidHom fixes a new toFun equal to the old one, preserving structure.

Русский

Конструктор копирования для StarMonoidHom задаёт новую функцию равной старой и сохраняет структуру.

LaTeX

$$$\\mathrm{StarMonoidHom.copy}\\ (f\\;: A \\to\\star\\,* B)\\ (f' : A \\to B)\\ (h : f' = f) : A \\to\\star\\,* B$$$

Lean4

/-- Copy of a `StarMonoidHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities. -/
protected def copy (f : A →⋆* B) (f' : A → B) (h : f' = f) : A →⋆* B
    where
  toFun := f'
  map_one' := h.symm ▸ map_one f
  map_mul' := h.symm ▸ map_mul f
  map_star' := h.symm ▸ map_star f

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