coe_copy_eq — Mathlib

English

The copy operation for MonoidHom respects equality of the underlying function: if f' equals the function of f, then f.copy f' h = f.

Русский

Операция копирования для MonoidHom сохраняет равенство по базовой функции: если f' совпадает с функцией f, то f.copy f' h = f.

LaTeX

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

Lean4

@[to_additive]
theorem coe_copy_eq {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

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