[Merged by Bors] - feat(field_theory/finite): Chevalley–Warning #1564
Conversation
jcommelin
commented
Oct 17, 2019
•
jcommelin
commented
|
I would be inclined to split off the items numbered 4 and 5 from |
|
The merge conflict is from this code, added to the deleted |
|
Thanks Bryan, I'll try to glue the pieces back together. |
There was a problem hiding this comment.
Oof, I underestimated how sticky this situation got. Sorry, I'm partly responsible for this mess. At this point, I think it is best to proceed in small steps. I suggest not doing any refactoring or variable renaming in this PR, and just adding the new content to a new file. I think the new content in field_theory.finite.basic is sum_pow_units, cast_card_eq_zero, sum_pow_lt_card_sub_one; probably you can verify this easily.
Since I'm already in the process of looking at this, I'll review it as though this has already happened.
src/field_theory/finite/basic.lean
Outdated
| have hq : 0 < q - 1, | ||
| { rw [← card_units, fintype.card_pos_iff], | ||
| exact ⟨1⟩ }, | ||
| cases is_cyclic.exists_generator (units K) with a ha, |
There was a problem hiding this comment.
You could write
let ⟨a, ha⟩ := is_cyclic.exists_generator (units K) in
calc ...and avoid "fake tactic mode".
There was a problem hiding this comment.
Mwah... there is so much tactic mode in this proof that I don't care about a little bit of fake tactic mode as well. (I know that calc is a fake tactic. But all the begin ... end blocks aren't)
Anyway, I can fix it if you prefer.
rwbarton
added
the
awaiting-author
|
@rwbarton Thanks a lot for the thorough review. I currently don't have any time to work on this. What I propose is that we first fix the |
…c 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.
|
Also, I would still prefer to remove those instances. |
|
@rwbarton I think I've done everything you suggested. |
jcommelin
added
awaiting-review
|
Is this really a PR asking to merge 79 commits? Or is there some git accident here? |
Many PRs were split off from this one. Note that in the current diff, only 4 files are changed. |
|
bors merge |
github-actions
bot
added
ready-to-merge
|
bors r- |
|
Canceled. |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…c search (leanprover-community#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 leanprover-community#1601 and leanprover-community#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 leanprover-community#1564.
…er-community#2560) A number a small changes that prepare for leanprover-community#1564.
