groups (#2844)

Commit

5 years ago

refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844) This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.

Author

jcommelin

Parents

f098c16e

mathlib3 1a4f0c22 - refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844)

mathlib3
1a4f0c22 - refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844)