copy — Mathlib

English

Copy of a linear map with a new underlying function; if the new function equals the old one, the copy equals the original.

Русский

Копия линейного отображения с новой действующей функцией; если новая функция равна старой, копия равна исходному отображению.

LaTeX

$$$f.copy\; f'\; h = f$$$

Lean4

/-- Copy of a `LinearMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃
    where
  toFun := f'
  map_add' := h.symm ▸ f.map_add'
  map_smul' := h.symm ▸ f.map_smul'

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