coe_monoidHom — Mathlib

English

Two OrderMonoidHom objects are equal if they have the same behavior as functions; i.e., if their underlying functions are equal, then the homomorphisms are equal.

Русский

Два объекта OrderMonoidHom равны, если они ведут одинаково как функции; если их базовые функции равны, то гомоморфизмы равны.

LaTeX

$$If f.toFun = g.toFun, then f = g$$

Lean4

@[to_additive (attr := simp)]
theorem coe_monoidHom (f : α →*o β) : ((f : α →* β) : α → β) = f :=
  rfl

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