Theorem OmegaCompletePartialOrder.Chain.zip_coe

Modification history

2026-04-02 17:24

Mathlib/Order/OmegaCompletePartialOrder.lean

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

Deleted OmegaCompletePartialOrder.Chain.zip_coe View on Github →

2023-07-31 23:05

Mathlib/Order/OmegaCompletePartialOrder.lean

chore: use `FunLike` for `OrderHom` (#5805)

Added OmegaCompletePartialOrder.Chain.zip_coe View on Github →