Commit 2026-04-02 17:24 fdfd405f

View on Github →

refactor(Order/OmegaCompletePartialOrder): make Chain a structure (#37258) It has a different LE to OrderHom, hence should not be an abbrev.

Estimated changes

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

added theorem OmegaCompletePartialOrder.Chain.coe_map

added theorem OmegaCompletePartialOrder.Chain.coe_toOrderHom

modified def OmegaCompletePartialOrder.Chain.map

deleted theorem OmegaCompletePartialOrder.Chain.map_coe

modified theorem OmegaCompletePartialOrder.Chain.map_id

modified theorem OmegaCompletePartialOrder.Chain.map_le_map

modified def OmegaCompletePartialOrder.Chain.zip

added theorem OmegaCompletePartialOrder.Chain.zip_apply

deleted theorem OmegaCompletePartialOrder.Chain.zip_coe

added structure OmegaCompletePartialOrder.Chain

deleted def OmegaCompletePartialOrder.Chain

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean