Documentation

Mathlib.Algebra.Order.Group.TypeTags

Ordered group structures on Multiplicative α and Additive α. #