MonoidWithZero

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

Statistics

Metric	Count
Definitions `unitsWithZero`, `withZero`, `withZeroUnits`, `OrderMonoidWithZeroHom`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `instMul`, `toMonoidWithZeroHom`, `toOrderMonoidHom`, `toOrderMonoidWithZeroHom`, `instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass`, `«term_→*₀o_»`	15
Theorems `unitsWithZero_apply`, `val_inv_unitsWithZero_symm_apply`, `val_unitsWithZero_symm_apply`, `withZeroUnits_apply`, `withZeroUnits_symm_apply`, `withZero_apply_apply`, `withZero_apply_symm_apply`, `withZero_symm_apply_apply`, `withZero_symm_apply_symm_apply`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_monoidWithZeroHom`, `coe_comp_orderMonoidHom`, `coe_copy`, `coe_id`, `coe_mk`, `coe_monoidWithZeroHom`, `coe_mul`, `coe_orderMonoidHom`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_mul`, `copy_eq`, `ext`, `ext_iff`, `id_comp`, `instMonoidWithZeroHomClass`, `instOrderHomClass`, `mk_coe`, `monotone'`, `mul_apply`, `mul_comp`, `toFun_eq_coe`, `toMonoidWithZeroHom_coe`, `toMonoidWithZeroHom_eq_coe`, `toMonoidWithZeroHom_injective`, `toMonoidWithZeroHom_mk`, `toOrderMonoidHom_comp`, `toOrderMonoidHom_eq_coe`, `toOrderMonoidHom_injective`	42
Total	57

OrderMonoidIso

Definitions

Name	Category	Theorems
`unitsWithZero` 📖	CompOp	3 math math: `val_inv_unitsWithZero_symm_apply`, `val_unitsWithZero_symm_apply`, `unitsWithZero_apply`
`withZero` 📖	CompOp	4 math math: `withZero_symm_apply_symm_apply`, `withZero_symm_apply_apply`, `withZero_apply_symm_apply`, `withZero_apply_apply`
`withZeroUnits` 📖	CompOp	2 math math: `withZeroUnits_symm_apply`, `withZeroUnits_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitsWithZero_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `Units` `WithZero` `MonoidWithZero.toMonoid` `WithZero.instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instPreorder` `WithZero.instPreorder` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `instEquivLike` `unitsWithZero` `WithZero.unzero` `Units.val`	—	—
`val_inv_unitsWithZero_symm_apply` 📖	mathematical	—	`Units.val` `WithZero` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `WithZero.instGroupWithZero` `Units` `Units.instInv` `DFunLike.coe` `OrderMonoidIso` `WithZero.instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instPreorder` `WithZero.instPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `unitsWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `WithZero.coe`	—	—
`val_unitsWithZero_symm_apply` 📖	mathematical	—	`Units.val` `WithZero` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `WithZero.instGroupWithZero` `DFunLike.coe` `OrderMonoidIso` `Units` `WithZero.instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instPreorder` `WithZero.instPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `unitsWithZero` `WithZero.coe`	—	—
`withZeroUnits_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `WithZero.instPreorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Units.instMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `EquivLike.toFunLike` `instEquivLike` `withZeroUnits` `WithZero.recZeroCoe` `MulZeroClass.toZero` `Units.val`	—	—
`withZeroUnits_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Units.instPreorder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroClass` `Units.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `withZeroUnits` `MulZeroClass.toZero` `WithZero.instZero` `WithZero.coe`	—	—
`withZero_apply_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `WithZero` `WithZero.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike` `withZero` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulEquiv.instEquivLike` `MulEquivClass.toMulEquiv` `instMulEquivClass`	—	—
`withZero_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `WithZero` `WithZero.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `Equiv.instEquivLike` `withZero` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulEquiv.instEquivLike` `MulEquiv.symm` `MulEquivClass.toMulEquiv` `instMulEquivClass`	—	—
`withZero_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `Equiv` `WithZero` `WithZero.instPreorder` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Equiv.instEquivLike` `Equiv.symm` `withZero` `WithZero.unzero` `WithZero.coe` `MulEquivClass.toMulEquiv`	—	—
`withZero_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidIso` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `WithZero` `WithZero.instPreorder` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Equiv.instEquivLike` `Equiv.symm` `withZero` `WithZero.unzero` `MulEquiv` `MulEquiv.instEquivLike` `MulEquiv.symm` `MulEquivClass.toMulEquiv` `WithZero.coe`	—	—

OrderMonoidWithZeroHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	14 math math: `coe_comp_orderMonoidHom`, `cancel_left`, `comp_assoc`, `comp_apply`, `mul_comp`, `coe_comp_monoidWithZeroHom`, `toMonoidWithZeroHom_coe`, `comp_id`, `coe_comp`, `LinearOrderedCommGroupWithZero.fst_comp_inl`, `toOrderMonoidHom_comp`, `id_comp`, `comp_mul`, `cancel_right`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	5 math math: `OrderRingHom.coe_orderMonoidWithZeroHom_id`, `comp_id`, `LinearOrderedCommGroupWithZero.fst_comp_inl`, `id_comp`, `coe_id`
`instFunLike` 📖	CompOp	28 math math: `coe_orderMonoidHom`, `toFun_eq_coe`, `coe_comp_orderMonoidHom`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `instMonoidWithZeroHomClass`, `comp_apply`, `toMonoidWithZeroHom_eq_coe`, `instOrderHomClass`, `coe_comp_monoidWithZeroHom`, `toMonoidWithZeroHom_coe`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `OrderRingHom.coe_coe_orderMonoidWithZeroHom`, `ext_iff`, `coe_comp`, `toMonoidWithZeroHom_mk`, `coe_mk`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `toOrderMonoidHom_comp`, `coe_mul`, `LinearOrderedCommGroupWithZero.fst_apply`, `OrderRingHom.coe_orderMonoidWithZeroHom_apply`, `toOrderMonoidHom_eq_coe`, `LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `coe_monoidWithZeroHom`, `coe_id`, `mul_apply`
`instInhabited` 📖	CompOp	—
`instMul` 📖	CompOp	4 math math: `mul_comp`, `coe_mul`, `comp_mul`, `mul_apply`
`toMonoidWithZeroHom` 📖	CompOp	4 math math: `toFun_eq_coe`, `toMonoidWithZeroHom_eq_coe`, `monotone'`, `toMonoidWithZeroHom_injective`
`toOrderMonoidHom` 📖	CompOp	2 math math: `toOrderMonoidHom_injective`, `toOrderMonoidHom_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike` `comp`	—	—
`coe_comp_monoidWithZeroHom` 📖	mathematical	—	`MonoidWithZeroHomClass.toMonoidWithZeroHom` `OrderMonoidWithZeroHom` `instFunLike` `instMonoidWithZeroHomClass` `comp` `MonoidWithZeroHom.comp`	—	`instMonoidWithZeroHomClass`
`coe_comp_orderMonoidHom` 📖	mathematical	—	`OrderMonoidHomClass.toOrderMonoidHom` `OrderMonoidWithZeroHom` `MulZeroOneClass.toMulOneClass` `instFunLike` `instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass` `comp` `OrderMonoidHom.comp`	—	`instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	`OrderMonoidHom` `MulZeroOneClass.toMulOneClass` `OrderMonoidHom.instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`Monotone` `ZeroHom.toFun` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZeroHom.toZeroHom`	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike`	—	—
`coe_monoidWithZeroHom` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `OrderMonoidWithZeroHom` `instFunLike` `instMonoidWithZeroHomClass`	—	`instMonoidWithZeroHomClass`
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `instFunLike` `instMul` `Pi.instMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass`	—	—
`coe_orderMonoidHom` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `MulZeroOneClass.toMulOneClass` `OrderMonoidHom.instFunLike` `OrderMonoidHomClass.toOrderMonoidHom` `OrderMonoidWithZeroHom` `instFunLike` `instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`	—	`instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_mul` 📖	mathematical	—	`comp` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `OrderMonoidWithZeroHom` `instMul`	—	`ext` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`
`copy_eq` 📖	mathematical	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	`copy` `OrderMonoidHomClass.toOrderMonoidHom` `MulZeroOneClass.toMulOneClass` `instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`	—	`DFunLike.ext'` `instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`
`ext` 📖	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`instMonoidWithZeroHomClass` 📖	mathematical	—	`MonoidWithZeroHomClass` `OrderMonoidWithZeroHom` `instFunLike`	—	`MonoidWithZeroHom.map_mul'` `MonoidWithZeroHom.map_one'` `ZeroHom.map_zero'`
`instOrderHomClass` 📖	mathematical	—	`OrderHomClass` `OrderMonoidWithZeroHom` `Preorder.toLE` `instFunLike`	—	`monotone'`
`mk_coe` 📖	—	`Monotone` `ZeroHom.toFun` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZeroHom.toZeroHom` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `OrderMonoidWithZeroHom` `instFunLike` `instMonoidWithZeroHomClass`	—	—	`instMonoidWithZeroHomClass`
`monotone'` 📖	mathematical	—	`Monotone` `ZeroHom.toFun` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZeroHom.toZeroHom` `toMonoidWithZeroHom`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `instFunLike` `instMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass`	—	—
`mul_comp` 📖	mathematical	—	`comp` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `OrderMonoidWithZeroHom` `instMul`	—	—
`toFun_eq_coe` 📖	mathematical	—	`ZeroHom.toFun` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZeroHom.toZeroHom` `toMonoidWithZeroHom` `DFunLike.coe` `OrderMonoidWithZeroHom` `instFunLike`	—	—
`toMonoidWithZeroHom_coe` 📖	mathematical	—	`MonoidWithZeroHomClass.toMonoidWithZeroHom` `OrderMonoidWithZeroHom` `instFunLike` `instMonoidWithZeroHomClass` `comp` `MonoidWithZeroHom.comp`	—	`instMonoidWithZeroHomClass`
`toMonoidWithZeroHom_eq_coe` 📖	mathematical	—	`toMonoidWithZeroHom` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `OrderMonoidWithZeroHom` `instFunLike` `instMonoidWithZeroHomClass`	—	—
`toMonoidWithZeroHom_injective` 📖	mathematical	—	`OrderMonoidWithZeroHom` `MonoidWithZeroHom` `toMonoidWithZeroHom`	—	`ext` `DFunLike.ext_iff`
`toMonoidWithZeroHom_mk` 📖	mathematical	`Monotone` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike`	`MonoidWithZeroHomClass.toMonoidWithZeroHom` `OrderMonoidWithZeroHom` `instFunLike` `instMonoidWithZeroHomClass`	—	`instMonoidWithZeroHomClass`
`toOrderMonoidHom_comp` 📖	mathematical	—	`OrderMonoidHomClass.toOrderMonoidHom` `OrderMonoidWithZeroHom` `MulZeroOneClass.toMulOneClass` `instFunLike` `instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass` `comp` `OrderMonoidHom.comp`	—	`instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`
`toOrderMonoidHom_eq_coe` 📖	mathematical	—	`toOrderMonoidHom` `OrderMonoidHomClass.toOrderMonoidHom` `OrderMonoidWithZeroHom` `MulZeroOneClass.toMulOneClass` `instFunLike` `instOrderHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `instMonoidWithZeroHomClass`	—	—
`toOrderMonoidHom_injective` 📖	mathematical	—	`OrderMonoidWithZeroHom` `OrderMonoidHom` `MulZeroOneClass.toMulOneClass` `toOrderMonoidHom`	—	`ext` `DFunLike.ext_iff`

OrderMonoidWithZeroHomClass

Definitions

Name	Category	Theorems
`toOrderMonoidWithZeroHom` 📖	CompOp	4 math math: `OrderRingHom.coe_orderMonoidWithZeroHom_id`, `OrderRingHom.coe_coe_orderMonoidWithZeroHom`, `OrderRingHom.toOrderMonoidWithZeroHom_eq_coe`, `OrderRingHom.coe_orderMonoidWithZeroHom_apply`

(root)

Definitions

Name	Category	Theorems
`OrderMonoidWithZeroHom` 📖	CompData	32 math math: `OrderMonoidWithZeroHom.coe_orderMonoidHom`, `OrderMonoidWithZeroHom.toFun_eq_coe`, `OrderMonoidWithZeroHom.coe_comp_orderMonoidHom`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `OrderMonoidWithZeroHom.instMonoidWithZeroHomClass`, `OrderMonoidWithZeroHom.comp_apply`, `OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe`, `OrderMonoidWithZeroHom.mul_comp`, `OrderMonoidWithZeroHom.instOrderHomClass`, `OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom`, `OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `OrderRingHom.coe_coe_orderMonoidWithZeroHom`, `OrderMonoidWithZeroHom.ext_iff`, `OrderMonoidWithZeroHom.coe_comp`, `OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk`, `OrderMonoidWithZeroHom.coe_mk`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `OrderMonoidWithZeroHom.toOrderMonoidHom_injective`, `OrderMonoidWithZeroHom.toOrderMonoidHom_comp`, `OrderMonoidWithZeroHom.coe_mul`, `LinearOrderedCommGroupWithZero.fst_apply`, `OrderRingHom.coe_orderMonoidWithZeroHom_apply`, `OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective`, `OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe`, `OrderMonoidWithZeroHom.comp_mul`, `LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `OrderMonoidWithZeroHom.coe_monoidWithZeroHom`, `OrderMonoidWithZeroHom.coe_id`, `OrderMonoidWithZeroHom.mul_apply`
`instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass` 📖	CompOp	—
`«term_→*₀o_»` 📖	CompOp	—

---

← Back to Index