mathlib

04948074 - feat(algebra/ordered_*): cleanup and projection notation (#3850)