Commit 2023-07-31 23:05 6c5ad83c

View on Github →

chore: use FunLike for OrderHom (#5805)

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/Control/LawfulFix.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/Order/Category/OmegaCompletePartialOrder.lean

Modified Mathlib/Order/Category/PartOrdCat.lean

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderHom.coe_eq

deleted theorem OrderHom.coe_fun_mk

added theorem OrderHom.coe_mk

added theorem OrderHom.toFun_eq_coe

added theorem OrderHomClass.coe_coe

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

added theorem OmegaCompletePartialOrder.Chain.map_coe

added theorem OmegaCompletePartialOrder.Chain.zip_coe

added theorem OmegaCompletePartialOrder.ContinuousHom.coe_apply

added theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk

added theorem OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom

modified def OmegaCompletePartialOrder.ContinuousHom.comp

modified theorem OmegaCompletePartialOrder.ContinuousHom.comp_id

modified def OmegaCompletePartialOrder.ContinuousHom.const

deleted theorem OmegaCompletePartialOrder.ContinuousHom.const_apply

added def OmegaCompletePartialOrder.ContinuousHom.copy

modified def OmegaCompletePartialOrder.ContinuousHom.id

modified theorem OmegaCompletePartialOrder.ContinuousHom.id_comp

deleted def OmegaCompletePartialOrder.ContinuousHom.ofFun

deleted def OmegaCompletePartialOrder.ContinuousHom.ofMono

added theorem OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean

added theorem Scott.IsOpen.isUpperSet

Modified Mathlib/Topology/Order/Hom/Esakia.lean

added theorem PseudoEpimorphism.toOrderHom_eq_coe