Commit 2025-08-22 16:06 5e7c0840
View on Github →feat(Algebra/Order): two auxiliary definitions (#28667) This PR introduces two constructors for isomorphisms of ordered monoids:
α ≃*o βgivesαˣ ≃*o βˣ(⊤ : Submonoid α) ≃*o α.
feat(Algebra/Order): two auxiliary definitions (#28667) This PR introduces two constructors for isomorphisms of ordered monoids:
α ≃*o β gives αˣ ≃*o βˣ(⊤ : Submonoid α) ≃*o α.