English
There is a copy operation that produces a new OrderMonoidWithZeroHom with a prescribed new function f' and a proof that f' equals the old one; this helps to fix definitional equalities.
Русский
Существуют копирующие конструкторы, создающие новый OrderMonoidWithZeroHom с заданной функцией f' и доказательством, что f'=старый, что упрощает выравнивание определений.
LaTeX
$$$\mathrm{OrderMonoidWithZeroHom.copy}(f,f',h) : \alpha \to_*_0β$ с $f' = f$$$
Lean4
/-- Copy of an `OrderMonoidWithZeroHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : α →*₀o β) (f' : α → β) (h : f' = f) : α →*o β :=
{ f.toOrderMonoidHom.copy f' h, f.toMonoidWithZeroHom.copy f' h with toFun := f' }
