copy — Mathlib

English

Copy of a nonunital star algebra homomorphism with a new underlying function.

Русский

Копия немономодного звёздно-алгебра-гомоморфизма с новой базовой функцией.

LaTeX

$$$\text{Copy}(f,A,B) = (f' : A \to B) \text{ s.t. } f' = f$$$

Lean4

/-- Copy of a `NonUnitalStarAlgHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities. -/
protected def copy (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = f) : A →⋆ₙₐ[R] B
    where
  toFun := f'
  map_smul' := h.symm ▸ map_smul f
  map_zero' := h.symm ▸ map_zero f
  map_add' := h.symm ▸ map_add f
  map_mul' := h.symm ▸ map_mul f
  map_star' := h.symm ▸ map_star f

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