instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass

English

Any type with OrderMonoidIsoClass can be cast into OrderMonoidIso via a default coercion.

Русский

Любой тип с OrderMonoidIsoClass может быть приведен к OrderMonoidIso через разумное приведение.

LaTeX

$$$\text{OrderMonoidIsoClass toOrderMonoidIso}$$$

Lean4

/-- Any type satisfying `OrderMonoidIsoClass` can be cast into `OrderMonoidIso` via
  `OrderMonoidIsoClass.toOrderMonoidIso`. -/
@[to_additive /-- Any type satisfying `OrderAddMonoidIsoClass` can be cast into `OrderAddMonoidIso`
      via `OrderAddMonoidIsoClass.toOrderAddMonoidIso`. -/
    ]
instance [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] : CoeTC F (α ≃*o β) :=
  ⟨OrderMonoidIsoClass.toOrderMonoidIso⟩

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