# Documentation

Mathlib.Algebra.Order.Group.TypeTags

# Ordered group structures on Multiplicative α and Additive α. #

instance Multiplicative.orderedCommGroup {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.