Theorem OmegaCompletePartialOrder.Chain.coe_toOrderHom

Modification history

2026-04-02 17:24

Mathlib/Order/OmegaCompletePartialOrder.lean

refactor(Order/OmegaCompletePartialOrder): make `Chain` a `structure` (#37258) …

Added OmegaCompletePartialOrder.Chain.coe_toOrderHom View on Github →