Commit 2020-04-24 23:37 e918f726

refactor(zmod): merge zmodp into zmod, use [fact p.prime] for tc search (#2511) This PR introduces the class fact P := P for P : Prop, which is a way to inject elementary propositions into the type class system. This desing is inspired by @cipher1024 's https://gist.github.com/cipher1024/9bd785a75384a4870b331714ec86ad6f#file-zmod_redesign-lean. We use this to endow zmod p with a field instance under the assumption [fact p.prime]. As a consequence, the type zmodp is no longer needed, which removes a lot of duplicate code. Besides that, we redefine zmod n, so that n is a natural number instead of a positive natural number, and zmod 0 is now definitionally the integers. To preserve computational properties, zmod n is not defined as quotient type, but rather as int and fin n, depending on whether n is 0 or (k+1). The rest of this PR is adapting the library to the new definitions (most notably quadratic reciprocity and Lagrange's four squares theorem). Future work: Refactor the padics to use [fact p.prime] instead of making nat.prime a class in those files. This will address #1601 and #1648. Once that is done, we can clean up the mess in char_p (where the imports are really tangled) and finally get some movement in #1564.