Theorem LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom

Modification history

2025-07-29 04:18
Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean
feat(Algebra/Order): Locally Finite Linearly Ordered Abelian Groups (#27430) …
Added LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHomView on Github →