Commit 2026-06-23 15:06 f5681a0c
View on Github →feat: Monoid and Group instances for OrderHom and OrderIso (#40515)
These will be used in an upcoming PR to turn fun x ↦ (x * · * star x) into a term of type R →* (R →o R) when R is a StarOrderedRing, and likewise also Rˣ →* (R ≃o R).