instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass

English

For any F with the appropriate FunLike, NonAssocSemiring and order/ring-hom class structure, there is a canonical instance that allows F to be coerced to OrderRingHom α β; i.e., there is a CoeTC F (α →+*o β).

Русский

Для любого F с необходимой структурой FunLike и соответствующими классами, существует канонический экземпляр, который позволяет F приводиться к OrderRingHom α β; т.е. существует CoeTC F (α →+*o β).

LaTeX

$$$\\text{CoeTC } F (\\alpha \\to+*o \\beta)$$$

Lean4

/-- Any type satisfying `OrderRingHomClass` can be cast into `OrderRingHom` via
  `OrderRingHomClass.toOrderRingHom`. -/
instance [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β]
    [RingHomClass F α β] : CoeTC F (α →+*o β) :=
  ⟨OrderRingHomClass.toOrderRingHom⟩

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