instMulEquivClass — Mathlib

English

The coe function of the constructor OrderMonoidIso.mk coincides with the given function, i.e., (OrderMonoidIso.mk f h : α → β) = f.

Русский

Функция извлечения из конструктора OrderMonoidIso.mk совпадает с данной функцией: (OrderMonoidIso.mk f h : α → β) = f.

LaTeX

$$$ (OrderMonoidIso.mk f h : \alpha \to β) = f $$$

Lean4

@[to_additive]
instance : MulEquivClass (α ≃*o β) α β where map_mul f := map_mul f.toMulEquiv

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