toOrderMonoidHom_eq_coe — Mathlib

English

For any f ∈ α →*₀o β, the canonical order-monoid-with-zero-hom f.toOrderMonoidHom is the same as f itself; i.e., f.toOrderMonoidHom = f.

Русский

Для любого f ∈ α →*₀o β канонический указатель на OrderMonoidWithZeroHom, получаемый функтором f.toOrderMonoidHom, совпадает с f; то есть f.toOrderMonoidHom = f.

LaTeX

$$$ f.toOrderMonoidHom = f $$$

Lean4

@[simp]
theorem toOrderMonoidHom_eq_coe (f : α →*₀o β) : f.toOrderMonoidHom = f :=
  rfl

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