Commit 2024-10-22 07:59 07013722

feat: WithAbs type synonym (#17998) This PR contains the type synonym WithAbs. This is a type synonym for a semiring R that depends on an absolute value v : AbsoluteValue R S, where S is an OrderedSemiring. This is used in order to handle ambiguities arising from multiple sources of instances. For example, each infinite place on a number field defines distinct uniform structures via their associated real absolute values. The WithAbs type synonym allows the type class inferencing system to automatically infer such dependent instances, making it simpler to define the Archimedean completions of a number field. See #16483 for this application along with prior feedback.