leanprover/lean — pull request #307 by avigad (2014-11-07 02:38:02+00:00)
Title: additive and multiplicative structures

I love the new structure command! I made a start on groups, and experimented with a new style for headers. (And yes, I am obsessive enough about these things that I am willing to revise all the files in the library, if we like it.)

Tomorrow I'll work on orders, and maybe adapt the function definition method used in nat.div to arbitrary well-founded orders.

After that, I'll work on rings, fields, and ordered rings and fields -- and then use these structures for nat and int.