# Commit 2020-04-24 23:37 e918f726

View on Github →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.