coe_copy — Mathlib

English

Let A and B be monoids with a star operation. If f: A →⋆* B is a star-monoid homomorphism and f': A → B is a function with h: f' = f, then the underlying map of the copy f.copy f' h is f'.

Русский

Пусть A и B — моноиды с операцией звезды. Пусть f: A →⋆* B — звёздный моноидный гомоморфизм, а f': A → B — функция, и имеется равенство h: f' = f. Тогда отображение, лежащее в основе копии f.copy f' h, равно f'.

LaTeX

$$$((f.copy\, f'\\, h) : A \\to B) = f'$$$

Lean4

@[simp]
theorem coe_copy (f : A →⋆* B) (f' : A → B) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

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