feat(data/zmod/quadratic_reciprocity): quadratic reciprocity #327
Conversation
|
Nice! |
algebra/group.lean
Outdated
| def units.mk_of_ne_zero [field α] {a : α} (ha : a ≠ 0) : units α := | ||
| ⟨a, a⁻¹, mul_inv_cancel ha, inv_mul_cancel ha⟩ | ||
|
|
||
| @[simp] lemma units.mk_of_ne_zero_inj {α : Type*} [field α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : |
There was a problem hiding this comment.
is there a reason to have {α : Type*} here and in the next lemma?
| @@ -42,7 +42,7 @@ by simp [finset.prod] | |||
| attribute [to_additive finset.sum_const_zero] prod_const_one | |||
|
|
|||
| @[simp, to_additive finset.sum_image] | |||
There was a problem hiding this comment.
I guess this and the next lemmas should be proven on multiset and then derived from this. Then these classical.dec_eq are not necessary anymore.
There was a problem hiding this comment.
Is this comment meant to be somewhere else? prod_image doesn't mention classical.dec_eq, and the decidable_eq is necessary to state the theorem. In general, what's the policy on lemmas that require decidability for the proof, but not the statement? I thought the policy was that classical logic was fine even when unnecessary, so there are a few lemmas where I just used classical.dec_eq in the proof, to save the small bother of a user having to provide the dec_eq.
There was a problem hiding this comment.
I've use that policy in a few places already. If the statement doesn't require decidable_eq, but the proof does, then you can use classical.dec_eq to locally assume it.
There was a problem hiding this comment.
Oh sorry, my comment on classical.dec_eq was unnecessary.
For me using classical.dec_eq is also fine, just a little bit annoying..
|
Chapeau! 🥂 |
|
Oh my god this is brilliant! |
Proof of the law of quadratic reciprocity,
Create
field_theory/finite, and prove the multiplicative group of a finite field is cyclicCreate
data/nat/totientalong with minor changes to other files that were necessary for the proof
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list