Monoid

📁 Source: Mathlib/Algebra/Order/Hom/Monoid.lean

Statistics

Metric	Count
Definitions `OrderAddMonoidHom`, `comp`, `copy`, `id`, `instAddOfIsOrderedAddMonoid`, `instFunLike`, `instInhabited`, `instZero`, `mk'`, `toAddMonoidHom`, `toOrderHom`, `OrderAddMonoidIso`, `apply`, `symm_apply`, `instEquivLike`, `instInhabited`, `mk'`, `refl`, `toAddEquiv`, `toOrderIso`, `trans`, `OrderMonoidHom`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `instMulOfIsOrderedMonoid`, `instOne`, `mk'`, `toMonoidHom`, `toOrderHom`, `toOrderAddMonoidHom`, `toOrderMonoidHom`, `OrderMonoidIso`, `apply`, `symm_apply`, `instEquivLike`, `instInhabited`, `mk'`, `refl`, `toMulEquiv`, `toOrderIso`, `trans`, `toOrderAddMonoidIso`, `toOrderMonoidIso`, `instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass`, `instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass`, `instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass`, `instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass`, `«term_→o_»`, `«term_→+o_»`, `«term_≃o_»`, `«term_≃+o_»`	54
Theorems `add_apply`, `add_comp`, `cancel_left`, `cancel_right`, `coe_add`, `coe_addMonoidHom`, `coe_comp`, `coe_comp_addMonoidHom`, `coe_comp_orderHom`, `coe_copy`, `coe_id`, `coe_mk`, `coe_orderHom`, `coe_zero`, `comp_add`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_zero`, `copy_eq`, `ext`, `ext_iff`, `id_comp`, `instAddMonoidHomClass`, `instOrderHomClass`, `mk_coe`, `monotone'`, `toAddMonoidHom_eq_coe`, `toAddMonoidHom_injective`, `toFun_eq_coe`, `toOrderHom_eq_coe`, `toOrderHom_injective`, `zero_apply`, `zero_comp`, `apply_eq_iff_symm_apply`, `apply_symm_apply`, `cancel_left`, `cancel_right`, `coe_addEquiv`, `coe_mk`, `coe_orderIso`, `coe_refl`, `coe_toEquiv_symm`, `coe_trans`, `coe_trans_addEquiv`, `coe_trans_orderIso`, `comp_symm_eq`, `eq_comp_symm`, `eq_symm_apply`, `eq_symm_comp`, `equivLike_neg_eq_symm`, `ext`, `ext_iff`, `instAddEquivClass`, `instOrderIsoClass`, `invFun_eq_symm`, `lt_symm_apply`, `map_le_map_iff'`, `mk_coe`, `refl_symm`, `refl_trans`, `self_comp_symm`, `strictMono`, `strictMono_symm`, `symm_apply_apply`, `symm_apply_eq`, `symm_apply_lt`, `symm_bijective`, `symm_comp_eq`, `symm_comp_self`, `symm_symm`, `toAddEquiv_eq_coe`, `toAddEquiv_injective`, `toEquiv_symm`, `toFun_eq_coe`, `toOrderIso_eq_coe`, `toOrderIso_injective`, `trans_apply`, `trans_assoc`, `trans_refl`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_monoidHom`, `coe_comp_orderHom`, `coe_copy`, `coe_id`, `coe_mk`, `coe_monoidHom`, `coe_mul`, `coe_one`, `coe_orderHom`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_mul`, `comp_one`, `copy_eq`, `ext`, `ext_iff`, `id_comp`, `instMonoidHomClass`, `instOrderHomClass`, `mk_coe`, `monotone'`, `mul_apply`, `mul_comp`, `one_apply`, `one_comp`, `toFun_eq_coe`, `toMonoidHom_eq_coe`, `toMonoidHom_injective`, `toOrderHom_eq_coe`, `toOrderHom_injective`, `apply_eq_iff_symm_apply`, `apply_symm_apply`, `cancel_left`, `cancel_right`, `coe_mk`, `coe_mulEquiv`, `coe_orderIso`, `coe_refl`, `coe_toEquiv_symm`, `coe_trans`, `coe_trans_mulEquiv`, `coe_trans_orderIso`, `comp_symm_eq`, `eq_comp_symm`, `eq_symm_apply`, `eq_symm_comp`, `equivLike_inv_eq_symm`, `ext`, `ext_iff`, `instMulEquivClass`, `instOrderIsoClass`, `invFun_eq_symm`, `lt_symm_apply`, `map_le_map_iff'`, `mk_coe`, `refl_symm`, `refl_trans`, `self_comp_symm`, `strictMono`, `strictMono_symm`, `symm_apply_apply`, `symm_apply_eq`, `symm_apply_lt`, `symm_bijective`, `symm_comp_eq`, `symm_comp_self`, `symm_symm`, `toEquiv_symm`, `toFun_eq_coe`, `toMulEquiv_eq_coe`, `toMulEquiv_injective`, `toOrderIso_eq_coe`, `toOrderIso_injective`, `trans_apply`, `trans_assoc`, `trans_refl`, `antitone_iff_map_nonneg`, `antitone_iff_map_nonpos`, `map_nonneg`, `map_nonpos`, `monotone_iff_map_nonneg`, `monotone_iff_map_nonpos`, `strictAnti_iff_map_neg`, `strictAnti_iff_map_pos`, `strictMono_iff_map_neg`, `strictMono_iff_map_pos`	170
Total	224

OrderAddMonoidHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	18 math math: `comp_zero`, `coe_comp_orderHom`, `fst_comp_inl`, `fstₗ_comp_inlₗ`, `coe_comp_addMonoidHom`, `snd_comp_inr`, `comp_add`, `add_comp`, `cancel_left`, `coe_comp`, `fst_comp_inr`, `cancel_right`, `id_comp`, `snd_comp_inl`, `comp_apply`, `comp_assoc`, `comp_id`, `zero_comp`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`id` 📖	CompOp	7 math math: `fst_comp_inl`, `OrderRingHom.coe_orderAddMonoidHom_id`, `fstₗ_comp_inlₗ`, `snd_comp_inr`, `id_comp`, `coe_id`, `comp_id`
`instAddOfIsOrderedAddMonoid` 📖	CompOp	4 math math: `add_apply`, `coe_add`, `comp_add`, `add_comp`
`instFunLike` 📖	CompOp	52 math math: `OrderRingHom.coe_orderAddMonoidHom_apply`, `inl_apply`, `coe_comp_orderHom`, `coe_orderHom`, `coe_copy`, `add_apply`, `Archimedean.embedReal_apply`, `addCommute_inlₗ_inrₗ`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `LocallyFiniteOrder.orderAddMonoidHom_bijective`, `coe_addMonoidHom`, `addCommute_inl_inr`, `ext_iff`, `coe_zero`, `ArchimedeanClass.orderHom_zero`, `ArchimedeanClass.map_mk_le`, `zero_apply`, `LocallyFiniteOrder.orderAddMonoidHom_strictMono`, `Archimedean.embedReal_injective`, `ArchimedeanClass.map_mk_eq`, `coe_add`, `HahnSeries.embDomainOrderAddMonoidHom_injective`, `OrderRingHom.coe_coe_orderAddMonoidHom`, `coe_comp_addMonoidHom`, `inlₗ_apply`, `DivisibleHull.coeOrderAddMonoidHom_apply`, `LocallyFiniteOrder.orderAddMonoidHom_apply`, `inlₗ_add_inrₗ_eq_toLex`, `ArchimedeanClass.mk_map_of_archimedean`, `Archimedean.exists_orderAddMonoidHom_real_injective`, `HahnSeries.embDomainOrderAddMonoidHom_apply`, `coe_comp`, `inr_apply`, `LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom`, `fstₗ_apply`, `inl_add_inr_eq_mk`, `snd_apply`, `instOrderHomClass`, `coe_id`, `ArchimedeanClass.orderHom_mk`, `Archimedean.embedReal_one`, `fst_apply`, `comp_apply`, `toFun_eq_coe`, `toOrderHom_eq_coe`, `coe_mk`, `inrₗ_apply`, `instAddMonoidHomClass`, `toAddMonoidHom_eq_coe`, `mk_coe`, `hahnEmbedding_isOrderedAddMonoid`, `HahnEmbedding.Partial.toOrderAddMonoidHom_injective`
`instInhabited` 📖	CompOp	—
`instZero` 📖	CompOp	6 math math: `comp_zero`, `coe_zero`, `zero_apply`, `fst_comp_inr`, `snd_comp_inl`, `zero_comp`
`mk'` 📖	CompOp	—
`toAddMonoidHom` 📖	CompOp	4 math math: `toAddMonoidHom_injective`, `monotone'`, `toFun_eq_coe`, `toAddMonoidHom_eq_coe`
`toOrderHom` 📖	CompOp	2 math math: `toOrderHom_injective`, `toOrderHom_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddOfIsOrderedAddMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`add_comp` 📖	mathematical	—	`comp` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `OrderAddMonoidHom` `instAddOfIsOrderedAddMonoid`	—	—
`cancel_left` 📖	mathematical	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `instAddOfIsOrderedAddMonoid` `Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`coe_addMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toAddMonoidHom` `OrderAddMonoidHom` `instFunLike` `instAddMonoidHomClass`	—	`instAddMonoidHomClass`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `comp`	—	—
`coe_comp_addMonoidHom` 📖	mathematical	—	`AddMonoidHomClass.toAddMonoidHom` `OrderAddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `instAddMonoidHomClass` `comp` `AddMonoidHom.comp`	—	`instAddMonoidHomClass`
`coe_comp_orderHom` 📖	mathematical	—	`OrderHomClass.toOrderHom` `OrderAddMonoidHom` `instFunLike` `instOrderHomClass` `comp` `OrderHom.comp`	—	`instOrderHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`Monotone` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidHom.toZeroHom`	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	—	—
`coe_orderHom` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHomClass.toOrderHom` `OrderAddMonoidHom` `instFunLike` `instOrderHomClass`	—	`instOrderHomClass`
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `instZero` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`comp_add` 📖	mathematical	—	`comp` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `OrderAddMonoidHom` `instAddOfIsOrderedAddMonoid`	—	`ext` `map_add` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_zero` 📖	mathematical	—	`comp` `OrderAddMonoidHom` `instZero`	—	`ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass`
`copy_eq` 📖	mathematical	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`instAddMonoidHomClass` 📖	mathematical	—	`AddMonoidHomClass` `OrderAddMonoidHom` `AddZeroClass.toAddZero` `instFunLike`	—	`AddMonoidHom.map_add'` `ZeroHom.map_zero'`
`instOrderHomClass` 📖	mathematical	—	`OrderHomClass` `OrderAddMonoidHom` `Preorder.toLE` `instFunLike`	—	`monotone'`
`mk_coe` 📖	mathematical	`Monotone` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidHom.toZeroHom` `AddMonoidHomClass.toAddMonoidHom` `OrderAddMonoidHom` `instFunLike` `instAddMonoidHomClass`	`AddMonoidHomClass.toAddMonoidHom` `OrderAddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `instAddMonoidHomClass`	—	`instAddMonoidHomClass` `ext`
`monotone'` 📖	mathematical	—	`Monotone` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidHom.toZeroHom` `toAddMonoidHom`	—	—
`toAddMonoidHom_eq_coe` 📖	mathematical	—	`toAddMonoidHom` `AddMonoidHomClass.toAddMonoidHom` `OrderAddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `instAddMonoidHomClass`	—	—
`toAddMonoidHom_injective` 📖	mathematical	—	`OrderAddMonoidHom` `AddMonoidHom` `AddZeroClass.toAddZero` `toAddMonoidHom`	—	`ext` `DFunLike.ext_iff`
`toFun_eq_coe` 📖	mathematical	—	`ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidHom.toZeroHom` `toAddMonoidHom` `DFunLike.coe` `OrderAddMonoidHom` `instFunLike`	—	—
`toOrderHom_eq_coe` 📖	mathematical	—	`toOrderHom` `OrderHomClass.toOrderHom` `OrderAddMonoidHom` `instFunLike` `instOrderHomClass`	—	—
`toOrderHom_injective` 📖	mathematical	—	`OrderAddMonoidHom` `OrderHom` `toOrderHom`	—	`ext` `DFunLike.ext_iff`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `instFunLike` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`zero_comp` 📖	mathematical	—	`comp` `OrderAddMonoidHom` `instZero`	—	—

OrderAddMonoidIso

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	35 math math: `symm_comp_self`, `toEquiv_symm`, `symm_comp_eq`, `strictMono_symm`, `eq_symm_comp`, `equivLike_neg_eq_symm`, `coe_trans_orderIso`, `coe_toEquiv_symm`, `symm_apply_eq`, `symm_apply_lt`, `coe_trans_addEquiv`, `eq_comp_symm`, `coe_addEquiv`, `coe_mk`, `self_comp_symm`, `toAddEquiv_eq_coe`, `apply_symm_apply`, `instAddEquivClass`, `comp_symm_eq`, `instOrderIsoClass`, `coe_trans`, `apply_eq_iff_symm_apply`, `coe_refl`, `toFun_eq_coe`, `ext_iff`, `lt_symm_apply`, `strictMono`, `invFun_eq_symm`, `toOrderIso_eq_coe`, `symm_apply_apply`, `trans_apply`, `coe_orderIso`, `LocallyFiniteOrder.orderAddMonoidEquiv_apply`, `mk_coe`, `eq_symm_apply`
`instInhabited` 📖	CompOp	—
`mk'` 📖	CompOp	—
`refl` 📖	CompOp	4 math math: `refl_symm`, `refl_trans`, `coe_refl`, `trans_refl`
`toAddEquiv` 📖	CompOp	5 math math: `toAddEquiv_injective`, `map_le_map_iff'`, `toAddEquiv_eq_coe`, `toFun_eq_coe`, `invFun_eq_symm`
`toOrderIso` 📖	CompOp	2 math math: `toOrderIso_eq_coe`, `toOrderIso_injective`
`trans` 📖	CompOp	9 math math: `cancel_right`, `coe_trans_orderIso`, `trans_assoc`, `coe_trans_addEquiv`, `refl_trans`, `coe_trans`, `trans_refl`, `trans_apply`, `cancel_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`cancel_left` 📖	mathematical	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike`	`trans`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`cancel_right` 📖	mathematical	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike`	`trans`	—	`ext` `trans_apply`
`coe_addEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.toAddEquiv` `OrderAddMonoidIso` `instEquivLike` `instAddEquivClass`	—	`instAddEquivClass`
`coe_mk` 📖	mathematical	`Preorder.toLE` `Equiv.toFun` `AddEquiv.toEquiv`	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `AddEquiv` `AddEquiv.instEquivLike`	—	—
`coe_orderIso` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHomClass.toOrderHom` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `OrderIsoClass.toOrderHomClass` `Preorder.toLE` `instOrderIsoClass`	—	`OrderIsoClass.toOrderHomClass` `instOrderIsoClass`
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`coe_toEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `EquivLike.toEquiv` `OrderAddMonoidIso` `instEquivLike` `symm`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`coe_trans_addEquiv` 📖	mathematical	—	`AddEquivClass.toAddEquiv` `OrderAddMonoidIso` `instEquivLike` `instAddEquivClass` `trans` `AddEquiv.trans`	—	`instAddEquivClass`
`coe_trans_orderIso` 📖	mathematical	—	`OrderIsoClass.toOrderIso` `OrderAddMonoidIso` `Preorder.toLE` `instEquivLike` `instOrderIsoClass` `trans` `OrderIso.trans`	—	`instOrderIsoClass`
`comp_symm_eq` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.comp_symm_eq`
`eq_comp_symm` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_comp_symm`
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_apply`
`eq_symm_comp` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_comp`
`equivLike_neg_eq_symm` 📖	mathematical	—	`EquivLike.inv` `OrderAddMonoidIso` `instEquivLike` `DFunLike.coe` `EquivLike.toFunLike` `symm`	—	—
`ext` 📖	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`instAddEquivClass` 📖	mathematical	—	`AddEquivClass` `OrderAddMonoidIso` `instEquivLike`	—	`map_add` `AddEquivClass.instAddHomClass` `AddEquiv.instAddEquivClass`
`instOrderIsoClass` 📖	mathematical	—	`OrderIsoClass` `OrderAddMonoidIso` `Preorder.toLE` `instEquivLike`	—	`map_le_map_iff'`
`invFun_eq_symm` 📖	mathematical	—	`Equiv.invFun` `AddEquiv.toEquiv` `toAddEquiv` `DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`lt_symm_apply` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`OrderIso.lt_symm_apply`
`map_le_map_iff'` 📖	mathematical	—	`Preorder.toLE` `Equiv.toFun` `AddEquiv.toEquiv` `toAddEquiv`	—	—
`mk_coe` 📖	mathematical	`Preorder.toLE` `Equiv.toFun` `AddEquiv.toEquiv` `AddEquivClass.toAddEquiv` `OrderAddMonoidIso` `instEquivLike` `instAddEquivClass`	`AddEquivClass.toAddEquiv` `OrderAddMonoidIso` `instEquivLike` `instAddEquivClass`	—	`instAddEquivClass`
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	—
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`apply_symm_apply`
`strictMono` 📖	mathematical	—	`StrictMono` `DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	`strictMono_of_le_iff_le` `OrderIsoClass.map_le_map_iff` `instOrderIsoClass`
`strictMono_symm` 📖	mathematical	—	`StrictMono` `DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`strictMono_of_le_iff_le` `OrderIsoClass.map_le_map_iff` `instOrderIsoClass` `Equiv.apply_symm_apply`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_apply_lt` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`OrderIso.symm_apply_lt`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `OrderAddMonoidIso` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_eq` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_comp_eq`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`symm_apply_apply`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`toAddEquiv_eq_coe` 📖	mathematical	—	`toAddEquiv` `AddEquivClass.toAddEquiv` `OrderAddMonoidIso` `instEquivLike` `instAddEquivClass`	—	—
`toAddEquiv_injective` 📖	mathematical	—	`OrderAddMonoidIso` `AddEquiv` `toAddEquiv`	—	`ext` `DFunLike.ext_iff`
`toEquiv_symm` 📖	mathematical	—	`EquivLike.toEquiv` `OrderAddMonoidIso` `instEquivLike` `symm` `Equiv.symm`	—	—
`toFun_eq_coe` 📖	mathematical	—	`Equiv.toFun` `AddEquiv.toEquiv` `toAddEquiv` `DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	—
`toOrderIso_eq_coe` 📖	mathematical	—	`toOrderIso` `OrderIsoClass.toOrderIso` `OrderAddMonoidIso` `Preorder.toLE` `instEquivLike` `instOrderIsoClass`	—	—
`toOrderIso_injective` 📖	mathematical	—	`OrderAddMonoidIso` `OrderIso` `Preorder.toLE` `toOrderIso`	—	`ext` `DFunLike.ext_iff`
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_assoc` 📖	mathematical	—	`trans`	—	—
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	—

OrderAddMonoidIso.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

OrderMonoidHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	20 math math: `OrderMonoidWithZeroHom.coe_comp_orderMonoidHom`, `comp_id`, `cancel_left`, `mul_comp`, `cancel_right`, `comp_assoc`, `comp_apply`, `id_comp`, `comp_one`, `coe_comp_monoidHom`, `coe_comp`, `OrderMonoidWithZeroHom.toOrderMonoidHom_comp`, `snd_comp_inl`, `snd_comp_inr`, `fstₗ_comp_inlₗ`, `coe_comp_orderHom`, `fst_comp_inr`, `fst_comp_inl`, `comp_mul`, `one_comp`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	6 math math: `comp_id`, `id_comp`, `coe_id`, `snd_comp_inr`, `fstₗ_comp_inlₗ`, `fst_comp_inl`
`instFunLike` 📖	CompOp	39 math math: `inl_mul_inr_eq_mk`, `OrderMonoidWithZeroHom.coe_orderMonoidHom`, `one_apply`, `mul_apply`, `instOrderHomClass`, `commute_inl_inr`, `toMonoidHom_eq_coe`, `MulArchimedeanClass.map_mk_le`, `toFun_eq_coe`, `inrₗ_apply`, `instMonoidHomClass`, `inlₗ_mul_inrₗ_eq_toLex`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `ext_iff`, `comp_apply`, `MulArchimedeanClass.map_mk_eq`, `inlₗ_apply`, `toOrderHom_eq_coe`, `coe_comp_monoidHom`, `coe_mul`, `fstₗ_apply`, `coe_copy`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `coe_comp`, `commute_inlₗ_inrₗ`, `snd_apply`, `inl_apply`, `coe_id`, `fst_apply`, `coe_one`, `LocallyFiniteOrder.orderMonoidHom_strictMono`, `coe_monoidHom`, `coe_comp_orderHom`, `OrderMonoidWithZeroHom.coe_copy`, `inr_apply`, `coe_mk`, `MulArchimedeanClass.orderHom_mk`, `coe_orderHom`, `mk_coe`
`instInhabited` 📖	CompOp	—
`instMulOfIsOrderedMonoid` 📖	CompOp	4 math math: `mul_apply`, `mul_comp`, `coe_mul`, `comp_mul`
`instOne` 📖	CompOp	6 math math: `one_apply`, `comp_one`, `snd_comp_inl`, `coe_one`, `fst_comp_inr`, `one_comp`
`mk'` 📖	CompOp	—
`toMonoidHom` 📖	CompOp	4 math math: `toMonoidHom_eq_coe`, `toMonoidHom_injective`, `toFun_eq_coe`, `monotone'`
`toOrderHom` 📖	CompOp	2 math math: `toOrderHom_eq_coe`, `toOrderHom_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `OrderMonoidHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `OrderMonoidHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `comp`	—	—
`coe_comp_monoidHom` 📖	mathematical	—	`MonoidHomClass.toMonoidHom` `OrderMonoidHom` `MulOneClass.toMulOne` `instFunLike` `instMonoidHomClass` `comp` `MonoidHom.comp`	—	`instMonoidHomClass`
`coe_comp_orderHom` 📖	mathematical	—	`OrderHomClass.toOrderHom` `OrderMonoidHom` `instFunLike` `instOrderHomClass` `comp` `OrderHom.comp`	—	`instOrderHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `OrderMonoidHom` `instFunLike`	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`Monotone` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MonoidHom.toOneHom`	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	—	—
`coe_monoidHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHomClass.toMonoidHom` `OrderMonoidHom` `instFunLike` `instMonoidHomClass`	—	`instMonoidHomClass`
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instMulOfIsOrderedMonoid` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `instOne` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`coe_orderHom` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHomClass.toOrderHom` `OrderMonoidHom` `instFunLike` `instOrderHomClass`	—	`instOrderHomClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_mul` 📖	mathematical	—	`comp` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `OrderMonoidHom` `instMulOfIsOrderedMonoid`	—	`ext` `map_mul` `MonoidHomClass.toMulHomClass` `instMonoidHomClass`
`comp_one` 📖	mathematical	—	`comp` `OrderMonoidHom` `instOne`	—	`ext` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass`
`copy_eq` 📖	mathematical	`DFunLike.coe` `OrderMonoidHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`instMonoidHomClass` 📖	mathematical	—	`MonoidHomClass` `OrderMonoidHom` `MulOneClass.toMulOne` `instFunLike`	—	`MonoidHom.map_mul'` `OneHom.map_one'`
`instOrderHomClass` 📖	mathematical	—	`OrderHomClass` `OrderMonoidHom` `Preorder.toLE` `instFunLike`	—	`monotone'`
`mk_coe` 📖	mathematical	`Monotone` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MonoidHom.toOneHom` `MonoidHomClass.toMonoidHom` `OrderMonoidHom` `instFunLike` `instMonoidHomClass`	`MonoidHomClass.toMonoidHom` `OrderMonoidHom` `MulOneClass.toMulOne` `instFunLike` `instMonoidHomClass`	—	`instMonoidHomClass` `ext`
`monotone'` 📖	mathematical	—	`Monotone` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MonoidHom.toOneHom` `toMonoidHom`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `instMulOfIsOrderedMonoid` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`mul_comp` 📖	mathematical	—	`comp` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `OrderMonoidHom` `instMulOfIsOrderedMonoid`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `instFunLike` `instOne` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`one_comp` 📖	mathematical	—	`comp` `OrderMonoidHom` `instOne`	—	—
`toFun_eq_coe` 📖	mathematical	—	`OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MonoidHom.toOneHom` `toMonoidHom` `DFunLike.coe` `OrderMonoidHom` `instFunLike`	—	—
`toMonoidHom_eq_coe` 📖	mathematical	—	`toMonoidHom` `MonoidHomClass.toMonoidHom` `OrderMonoidHom` `MulOneClass.toMulOne` `instFunLike` `instMonoidHomClass`	—	—
`toMonoidHom_injective` 📖	mathematical	—	`OrderMonoidHom` `MonoidHom` `MulOneClass.toMulOne` `toMonoidHom`	—	`ext` `DFunLike.ext_iff`
`toOrderHom_eq_coe` 📖	mathematical	—	`toOrderHom` `OrderHomClass.toOrderHom` `OrderMonoidHom` `instFunLike` `instOrderHomClass`	—	—
`toOrderHom_injective` 📖	mathematical	—	`OrderMonoidHom` `OrderHom` `toOrderHom`	—	`ext` `DFunLike.ext_iff`

OrderMonoidHomClass

Definitions

Name	Category	Theorems
`toOrderAddMonoidHom` 📖	CompOp	4 math math: `OrderRingHom.coe_orderAddMonoidHom_apply`, `OrderRingHom.coe_orderAddMonoidHom_id`, `OrderRingHom.toOrderAddMonoidHom_eq_coe`, `OrderRingHom.coe_coe_orderAddMonoidHom`
`toOrderMonoidHom` 📖	CompOp	5 math math: `OrderMonoidWithZeroHom.coe_orderMonoidHom`, `OrderMonoidWithZeroHom.coe_comp_orderMonoidHom`, `OrderMonoidWithZeroHom.toOrderMonoidHom_comp`, `OrderMonoidWithZeroHom.copy_eq`, `OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe`

OrderMonoidIso

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	66 math math: `apply_symm_apply`, `val_inv_unitsWithZero_symm_apply`, `WithVal.valueGroupOrderIso₀_symm_apply`, `withZero_symm_apply_symm_apply`, `withZero_symm_apply_apply`, `WithVal.valueGroupOrderIso₀_restrict`, `val_unitsCongr_symm_apply`, `WithVal.valueGroupOrderIso₀_apply`, `trans_apply`, `Submonoid.topOrderMonoidIso_symm_apply_coe`, `invFun_eq_symm`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀`, `instMulEquivClass`, `val_unitsCongr_apply`, `ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso`, `coe_mulEquiv`, `symm_apply_apply`, `symm_comp_self`, `val_inv_unitsCongr_symm_apply`, `withZeroUnits_symm_apply`, `withZeroUnits_apply`, `equivLike_inv_eq_symm`, `val_unitsWithZero_symm_apply`, `coe_mk`, `eq_symm_apply`, `WithVal.strictMono_valueGroupOrderIso₀`, `withZero_apply_symm_apply`, `WithVal.strictMono_valueGroupOrderIso₀_symm`, `symm_comp_eq`, `coe_orderIso`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk`, `PNat.equivNonZeroDivisorsNat_symm_apply_coe`, `unitsWithZero_apply`, `toMulEquiv_eq_coe`, `strictMono_symm`, `val_inv_unitsCongr_apply`, `withZero_apply_apply`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed`, `toOrderIso_eq_coe`, `self_comp_symm`, `apply_eq_iff_symm_apply`, `coe_trans_orderIso`, `comp_symm_eq`, `symm_apply_eq`, `toFun_eq_coe`, `instOrderIsoClass`, `PNat.equivNonZeroDivisorsNat_apply_coe`, `symm_apply_lt`, `mk_coe`, `strictMono`, `WithVal.valueGroupOrderIso₀_symm_restrict`, `ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq`, `coe_toEquiv_symm`, `coe_trans`, `coe_refl`, `ValuativeRel.valuation_lt_symm_orderMonoidIso`, `ValuativeRel.restrict_lt_orderMonoidIso`, `Valuation.IsEquiv.orderMonoidIso_spec`, `eq_symm_comp`, `Submonoid.topOrderMonoidIso_apply`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono`, `lt_symm_apply`, `eq_comp_symm`, `toEquiv_symm`, `ext_iff`, `coe_trans_mulEquiv`
`instInhabited` 📖	CompOp	—
`mk'` 📖	CompOp	—
`refl` 📖	CompOp	5 math math: `refl_symm`, `trans_refl`, `refl_trans`, `Valuation.IsEquiv.orderMonoidIso_eq_refl`, `coe_refl`
`toMulEquiv` 📖	CompOp	5 math math: `invFun_eq_symm`, `map_le_map_iff'`, `toMulEquiv_eq_coe`, `toFun_eq_coe`, `toMulEquiv_injective`
`toOrderIso` 📖	CompOp	2 math math: `toOrderIso_injective`, `toOrderIso_eq_coe`
`trans` 📖	CompOp	10 math math: `cancel_left`, `trans_apply`, `trans_assoc`, `cancel_right`, `Valuation.IsEquiv.orderMonoidIso_trans`, `coe_trans_orderIso`, `trans_refl`, `refl_trans`, `coe_trans`, `coe_trans_mulEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`cancel_left` 📖	mathematical	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike`	`trans`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`cancel_right` 📖	mathematical	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike`	`trans`	—	`ext` `trans_apply`
`coe_mk` 📖	mathematical	`Preorder.toLE` `Equiv.toFun` `MulEquiv.toEquiv`	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `MulEquiv` `MulEquiv.instEquivLike`	—	—
`coe_mulEquiv` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.toMulEquiv` `OrderMonoidIso` `instEquivLike` `instMulEquivClass`	—	`instMulEquivClass`
`coe_orderIso` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHomClass.toOrderHom` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `OrderIsoClass.toOrderHomClass` `Preorder.toLE` `instOrderIsoClass`	—	`OrderIsoClass.toOrderHomClass` `instOrderIsoClass`
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`coe_toEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `EquivLike.toEquiv` `OrderMonoidIso` `instEquivLike` `symm`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`coe_trans_mulEquiv` 📖	mathematical	—	`MulEquivClass.toMulEquiv` `OrderMonoidIso` `instEquivLike` `instMulEquivClass` `trans` `MulEquiv.trans`	—	`instMulEquivClass`
`coe_trans_orderIso` 📖	mathematical	—	`OrderIsoClass.toOrderIso` `OrderMonoidIso` `Preorder.toLE` `instEquivLike` `instOrderIsoClass` `trans` `OrderIso.trans`	—	`instOrderIsoClass`
`comp_symm_eq` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.comp_symm_eq`
`eq_comp_symm` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_comp_symm`
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_apply`
`eq_symm_comp` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_comp`
`equivLike_inv_eq_symm` 📖	mathematical	—	`EquivLike.inv` `OrderMonoidIso` `instEquivLike` `DFunLike.coe` `EquivLike.toFunLike` `symm`	—	—
`ext` 📖	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`instMulEquivClass` 📖	mathematical	—	`MulEquivClass` `OrderMonoidIso` `instEquivLike`	—	`map_mul` `MulEquivClass.instMulHomClass` `MulEquiv.instMulEquivClass`
`instOrderIsoClass` 📖	mathematical	—	`OrderIsoClass` `OrderMonoidIso` `Preorder.toLE` `instEquivLike`	—	`map_le_map_iff'`
`invFun_eq_symm` 📖	mathematical	—	`Equiv.invFun` `MulEquiv.toEquiv` `toMulEquiv` `DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`lt_symm_apply` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`OrderIso.lt_symm_apply`
`map_le_map_iff'` 📖	mathematical	—	`Preorder.toLE` `Equiv.toFun` `MulEquiv.toEquiv` `toMulEquiv`	—	—
`mk_coe` 📖	mathematical	`Preorder.toLE` `Equiv.toFun` `MulEquiv.toEquiv` `MulEquivClass.toMulEquiv` `OrderMonoidIso` `instEquivLike` `instMulEquivClass`	`MulEquivClass.toMulEquiv` `OrderMonoidIso` `instEquivLike` `instMulEquivClass`	—	`instMulEquivClass`
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	—
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`apply_symm_apply`
`strictMono` 📖	mathematical	—	`StrictMono` `DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	`strictMono_of_le_iff_le` `OrderIsoClass.map_le_map_iff` `instOrderIsoClass`
`strictMono_symm` 📖	mathematical	—	`StrictMono` `DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`strictMono_of_le_iff_le` `OrderIsoClass.map_le_map_iff` `instOrderIsoClass` `Equiv.apply_symm_apply`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_apply_lt` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`OrderIso.symm_apply_lt`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `OrderMonoidIso` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_eq` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_comp_eq`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`symm_apply_apply`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`toEquiv_symm` 📖	mathematical	—	`EquivLike.toEquiv` `OrderMonoidIso` `instEquivLike` `symm` `Equiv.symm`	—	—
`toFun_eq_coe` 📖	mathematical	—	`Equiv.toFun` `MulEquiv.toEquiv` `toMulEquiv` `DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike`	—	—
`toMulEquiv_eq_coe` 📖	mathematical	—	`toMulEquiv` `MulEquivClass.toMulEquiv` `OrderMonoidIso` `instEquivLike` `instMulEquivClass`	—	—
`toMulEquiv_injective` 📖	mathematical	—	`OrderMonoidIso` `MulEquiv` `toMulEquiv`	—	`ext` `DFunLike.ext_iff`
`toOrderIso_eq_coe` 📖	mathematical	—	`toOrderIso` `OrderIsoClass.toOrderIso` `OrderMonoidIso` `Preorder.toLE` `instEquivLike` `instOrderIsoClass`	—	—
`toOrderIso_injective` 📖	mathematical	—	`OrderMonoidIso` `OrderIso` `Preorder.toLE` `toOrderIso`	—	`ext` `DFunLike.ext_iff`
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_assoc` 📖	mathematical	—	`trans`	—	—
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	—

OrderMonoidIso.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

OrderMonoidIsoClass

Definitions

Name	Category	Theorems
`toOrderAddMonoidIso` 📖	CompOp	—
`toOrderMonoidIso` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`OrderAddMonoidHom` 📖	CompData	60 math math: `OrderRingHom.coe_orderAddMonoidHom_apply`, `OrderAddMonoidHom.comp_zero`, `OrderAddMonoidHom.inl_apply`, `OrderAddMonoidHom.coe_comp_orderHom`, `OrderAddMonoidHom.toAddMonoidHom_injective`, `OrderAddMonoidHom.coe_orderHom`, `OrderAddMonoidHom.coe_copy`, `OrderAddMonoidHom.add_apply`, `Archimedean.embedReal_apply`, `OrderAddMonoidHom.addCommute_inlₗ_inrₗ`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `LocallyFiniteOrder.orderAddMonoidHom_bijective`, `OrderAddMonoidHom.coe_addMonoidHom`, `OrderAddMonoidHom.addCommute_inl_inr`, `OrderAddMonoidHom.ext_iff`, `OrderAddMonoidHom.coe_zero`, `ArchimedeanClass.orderHom_zero`, `ArchimedeanClass.map_mk_le`, `OrderAddMonoidHom.zero_apply`, `LocallyFiniteOrder.orderAddMonoidHom_strictMono`, `Archimedean.embedReal_injective`, `ArchimedeanClass.map_mk_eq`, `OrderAddMonoidHom.coe_add`, `HahnSeries.embDomainOrderAddMonoidHom_injective`, `OrderRingHom.coe_coe_orderAddMonoidHom`, `OrderAddMonoidHom.coe_comp_addMonoidHom`, `OrderAddMonoidHom.inlₗ_apply`, `DivisibleHull.coeOrderAddMonoidHom_apply`, `OrderAddMonoidHom.comp_add`, `LocallyFiniteOrder.orderAddMonoidHom_apply`, `OrderAddMonoidHom.toOrderHom_injective`, `OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex`, `OrderAddMonoidHom.add_comp`, `ArchimedeanClass.mk_map_of_archimedean`, `Archimedean.exists_orderAddMonoidHom_real_injective`, `HahnSeries.embDomainOrderAddMonoidHom_apply`, `OrderAddMonoidHom.coe_comp`, `OrderAddMonoidHom.inr_apply`, `OrderAddMonoidHom.fst_comp_inr`, `LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom`, `OrderAddMonoidHom.fstₗ_apply`, `OrderAddMonoidHom.inl_add_inr_eq_mk`, `OrderAddMonoidHom.snd_apply`, `OrderAddMonoidHom.instOrderHomClass`, `OrderAddMonoidHom.snd_comp_inl`, `OrderAddMonoidHom.coe_id`, `ArchimedeanClass.orderHom_mk`, `Archimedean.embedReal_one`, `OrderAddMonoidHom.fst_apply`, `OrderAddMonoidHom.comp_apply`, `OrderAddMonoidHom.toFun_eq_coe`, `OrderAddMonoidHom.toOrderHom_eq_coe`, `OrderAddMonoidHom.coe_mk`, `OrderAddMonoidHom.inrₗ_apply`, `OrderAddMonoidHom.instAddMonoidHomClass`, `OrderAddMonoidHom.toAddMonoidHom_eq_coe`, `OrderAddMonoidHom.mk_coe`, `hahnEmbedding_isOrderedAddMonoid`, `OrderAddMonoidHom.zero_comp`, `HahnEmbedding.Partial.toOrderAddMonoidHom_injective`
`OrderAddMonoidIso` 📖	CompData	43 math math: `OrderAddMonoidIso.toAddEquiv_injective`, `LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete`, `OrderAddMonoidIso.symm_comp_self`, `OrderAddMonoidIso.toEquiv_symm`, `OrderAddMonoidIso.symm_comp_eq`, `OrderAddMonoidIso.strictMono_symm`, `OrderAddMonoidIso.eq_symm_comp`, `OrderAddMonoidIso.equivLike_neg_eq_symm`, `OrderAddMonoidIso.coe_trans_orderIso`, `OrderAddMonoidIso.coe_toEquiv_symm`, `OrderAddMonoidIso.symm_apply_eq`, `OrderAddMonoidIso.symm_apply_lt`, `OrderAddMonoidIso.coe_trans_addEquiv`, `OrderAddMonoidIso.eq_comp_symm`, `OrderAddMonoidIso.coe_addEquiv`, `OrderAddMonoidIso.coe_mk`, `OrderAddMonoidIso.self_comp_symm`, `LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered`, `OrderAddMonoidIso.toAddEquiv_eq_coe`, `OrderAddMonoidIso.symm_bijective`, `OrderAddMonoidIso.apply_symm_apply`, `OrderAddMonoidIso.instAddEquivClass`, `LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete`, `OrderAddMonoidIso.comp_symm_eq`, `OrderAddMonoidIso.instOrderIsoClass`, `OrderAddMonoidIso.coe_trans`, `OrderAddMonoidIso.apply_eq_iff_symm_apply`, `OrderAddMonoidIso.coe_refl`, `OrderAddMonoidIso.toFun_eq_coe`, `OrderAddMonoidIso.ext_iff`, `LinearOrderedAddCommGroup.discrete_or_denselyOrdered`, `OrderAddMonoidIso.lt_symm_apply`, `OrderAddMonoidIso.strictMono`, `OrderAddMonoidIso.invFun_eq_symm`, `OrderAddMonoidIso.toOrderIso_eq_coe`, `OrderAddMonoidIso.symm_apply_apply`, `OrderAddMonoidIso.trans_apply`, `OrderAddMonoidIso.coe_orderIso`, `LocallyFiniteOrder.orderAddMonoidEquiv_apply`, `LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int`, `OrderAddMonoidIso.toOrderIso_injective`, `OrderAddMonoidIso.mk_coe`, `OrderAddMonoidIso.eq_symm_apply`
`OrderMonoidHom` 📖	CompData	48 math math: `OrderMonoidHom.inl_mul_inr_eq_mk`, `OrderMonoidWithZeroHom.coe_orderMonoidHom`, `OrderMonoidHom.one_apply`, `OrderMonoidHom.mul_apply`, `OrderMonoidHom.instOrderHomClass`, `OrderMonoidHom.mul_comp`, `OrderMonoidHom.commute_inl_inr`, `OrderMonoidHom.toMonoidHom_eq_coe`, `OrderMonoidHom.toMonoidHom_injective`, `MulArchimedeanClass.map_mk_le`, `OrderMonoidHom.toFun_eq_coe`, `OrderMonoidHom.inrₗ_apply`, `OrderMonoidHom.instMonoidHomClass`, `OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `OrderMonoidHom.ext_iff`, `OrderMonoidHom.comp_apply`, `MulArchimedeanClass.map_mk_eq`, `OrderMonoidHom.comp_one`, `OrderMonoidHom.inlₗ_apply`, `OrderMonoidHom.toOrderHom_eq_coe`, `OrderMonoidHom.coe_comp_monoidHom`, `OrderMonoidHom.coe_mul`, `OrderMonoidHom.fstₗ_apply`, `OrderMonoidHom.coe_copy`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `OrderMonoidHom.coe_comp`, `OrderMonoidHom.commute_inlₗ_inrₗ`, `OrderMonoidWithZeroHom.toOrderMonoidHom_injective`, `OrderMonoidHom.snd_comp_inl`, `OrderMonoidHom.snd_apply`, `OrderMonoidHom.inl_apply`, `OrderMonoidHom.coe_id`, `OrderMonoidHom.fst_apply`, `OrderMonoidHom.coe_one`, `LocallyFiniteOrder.orderMonoidHom_strictMono`, `OrderMonoidHom.coe_monoidHom`, `OrderMonoidHom.coe_comp_orderHom`, `OrderMonoidWithZeroHom.coe_copy`, `OrderMonoidHom.fst_comp_inr`, `OrderMonoidHom.inr_apply`, `OrderMonoidHom.coe_mk`, `MulArchimedeanClass.orderHom_mk`, `OrderMonoidHom.coe_orderHom`, `OrderMonoidHom.mk_coe`, `OrderMonoidHom.comp_mul`, `OrderMonoidHom.toOrderHom_injective`, `OrderMonoidHom.one_comp`
`OrderMonoidIso` 📖	CompData	80 math math: `OrderMonoidIso.apply_symm_apply`, `OrderMonoidIso.val_inv_unitsWithZero_symm_apply`, `WithVal.valueGroupOrderIso₀_symm_apply`, `OrderMonoidIso.withZero_symm_apply_symm_apply`, `OrderMonoidIso.withZero_symm_apply_apply`, `WithVal.valueGroupOrderIso₀_restrict`, `OrderMonoidIso.val_unitsCongr_symm_apply`, `WithVal.valueGroupOrderIso₀_apply`, `OrderMonoidIso.trans_apply`, `Submonoid.topOrderMonoidIso_symm_apply_coe`, `OrderMonoidIso.invFun_eq_symm`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀`, `ValuativeRel.nonempty_orderIso_withZeroMul_int_iff`, `OrderMonoidIso.instMulEquivClass`, `OrderMonoidIso.val_unitsCongr_apply`, `ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso`, `OrderMonoidIso.coe_mulEquiv`, `OrderMonoidIso.symm_apply_apply`, `OrderMonoidIso.symm_comp_self`, `OrderMonoidIso.val_inv_unitsCongr_symm_apply`, `OrderMonoidIso.withZeroUnits_symm_apply`, `OrderMonoidIso.withZeroUnits_apply`, `OrderMonoidIso.equivLike_inv_eq_symm`, `OrderMonoidIso.val_unitsWithZero_symm_apply`, `OrderMonoidIso.coe_mk`, `OrderMonoidIso.eq_symm_apply`, `WithVal.strictMono_valueGroupOrderIso₀`, `OrderMonoidIso.withZero_apply_symm_apply`, `WithVal.strictMono_valueGroupOrderIso₀_symm`, `OrderMonoidIso.symm_comp_eq`, `OrderMonoidIso.coe_orderIso`, `LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk`, `PNat.equivNonZeroDivisorsNat_symm_apply_coe`, `OrderMonoidIso.unitsWithZero_apply`, `OrderMonoidIso.toMulEquiv_eq_coe`, `OrderMonoidIso.strictMono_symm`, `OrderMonoidIso.toOrderIso_injective`, `OrderMonoidIso.val_inv_unitsCongr_apply`, `OrderMonoidIso.withZero_apply_apply`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed`, `OrderMonoidIso.toOrderIso_eq_coe`, `LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete`, `OrderMonoidIso.self_comp_symm`, `OrderMonoidIso.apply_eq_iff_symm_apply`, `OrderMonoidIso.coe_trans_orderIso`, `OrderMonoidIso.comp_symm_eq`, `OrderMonoidIso.symm_apply_eq`, `OrderMonoidIso.toFun_eq_coe`, `OrderMonoidIso.instOrderIsoClass`, `PNat.equivNonZeroDivisorsNat_apply_coe`, `OrderMonoidIso.symm_apply_lt`, `OrderMonoidIso.mk_coe`, `OrderMonoidIso.strictMono`, `LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero`, `WithVal.valueGroupOrderIso₀_symm_restrict`, `ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq`, `OrderMonoidIso.coe_toEquiv_symm`, `Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange`, `OrderMonoidIso.coe_trans`, `OrderMonoidIso.coe_refl`, `ValuativeRel.valuation_lt_symm_orderMonoidIso`, `OrderMonoidIso.toMulEquiv_injective`, `OrderMonoidIso.symm_bijective`, `ValuativeRel.restrict_lt_orderMonoidIso`, `Valuation.IsEquiv.orderMonoidIso_spec`, `OrderMonoidIso.eq_symm_comp`, `Submonoid.topOrderMonoidIso_apply`, `LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered`, `LinearOrderedCommGroup.discrete_or_denselyOrdered`, `LinearOrderedCommGroup.discrete_iff_not_denselyOrdered`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono`, `OrderMonoidIso.lt_symm_apply`, `LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero`, `OrderMonoidIso.eq_comp_symm`, `OrderMonoidIso.toEquiv_symm`, `LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered`, `OrderMonoidIso.ext_iff`, `LinearOrderedCommGroup.isCyclic_iff_nonempty_equiv_int`, `OrderMonoidIso.coe_trans_mulEquiv`
`instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass` 📖	CompOp	—
`instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass` 📖	CompOp	—
`instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass` 📖	CompOp	—
`instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass` 📖	CompOp	—
`«term_→*o_»` 📖	CompOp	—
`«term_→+o_»` 📖	CompOp	—
`«term_≃*o_»` 📖	CompOp	—
`«term_≃+o_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_iff_map_nonneg` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLE` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`monotone_comp_ofDual_iff` `monotone_iff_map_nonneg` `OrderDual.isOrderedAddMonoid`
`antitone_iff_map_nonpos` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLE` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`monotone_toDual_comp_iff` `monotone_iff_map_nonneg` `OrderDual.isOrderedAddMonoid`
`map_nonneg` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE` `DFunLike.coe`	—	`map_zero` `OrderHomClass.mono`
`map_nonpos` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE` `DFunLike.coe`	—	`map_zero` `OrderHomClass.mono`
`monotone_iff_map_nonneg` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLE` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `sub_add_cancel` `map_add` `AddMonoidHomClass.toAddHomClass` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_nonneg`
`monotone_iff_map_nonpos` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLE` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`antitone_comp_ofDual_iff` `antitone_iff_map_nonpos` `OrderDual.isOrderedAddMonoid`
`strictAnti_iff_map_neg` 📖	mathematical	—	`StrictAnti` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`strictMono_toDual_comp_iff` `strictMono_iff_map_pos` `OrderDual.isOrderedAddMonoid`
`strictAnti_iff_map_pos` 📖	mathematical	—	`StrictAnti` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`strictMono_comp_ofDual_iff` `strictMono_iff_map_pos` `OrderDual.isOrderedAddMonoid`
`strictMono_iff_map_neg` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`strictAnti_comp_ofDual_iff` `strictAnti_iff_map_neg` `OrderDual.isOrderedAddMonoid`
`strictMono_iff_map_pos` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `DFunLike.coe` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `sub_add_cancel` `map_add` `AddMonoidHomClass.toAddHomClass` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `AddGroup.covconv` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `covariant_swap_add_of_covariant_add` `sub_pos`

---

← Back to Index