| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
| |
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
|
|
|
|
|
|
|
|
| |
The standard library uses Z.*, and Z* and Z_* are compatibility
notations. We follow suit.
Also, eliminate a few lemmas that are duplicates of ones in the standard
library.
|
| |
|
| |
|
|
|
|
| |
general contexts.
|
|
and finished encoding admits.
|