coe_mulEquiv — Mathlib

English

The underlying function of an ordered monoid isomorphism, when viewed as a plain multiplicative equivalence, is exactly the same function as the original map.

Русский

Лежащая в основе функция упорядоченного моноидного изоморфизма, когда её рассматривать как обычное умножаемое эквивалентное отображение, совпадает с исходной функцией.

LaTeX

$$$((f : α \simeq^*o β) : α \simeq^* β) : α \to β$ имеет ту же функциональность, что и $f$; то есть $((f : α \simeq^* β) : α \to β) = f$.$$

Lean4

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

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