mathlib documentation

algebra.order.group.type_tags

Ordered group structures on multiplicative α and additive α. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.