mk_coe — Mathlib

English

The auxiliary constructor mk with the coerced function equals the original structure; the resulting ordered monoid with zero homomorphism is identical to f.

Русский

Вспомогательный конструктор mk с приведённой функцией равен исходной структуре; полученный ордерированный моноид с нулём гомоморфизм совпадает с f.

LaTeX

$$$\mathrm{OrderMonoidWithZeroHom.mk}(f : \alpha \to_*_0 β)\; h = f$$$

Lean4

@[simp]
theorem mk_coe (f : α →*₀o β) (h) : OrderMonoidWithZeroHom.mk (f : α →*₀ β) h = f :=
  rfl

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