[Merged by Bors] - feat(number_theory/legendre_symbol/*): add results on value at -1 #13978
Conversation
MichaelStollBayreuth
added
the
awaiting-review
| @@ -43,7 +43,7 @@ begin | |||
| simp only [int.nat_abs_sq, int.coe_nat_pow, int.coe_nat_succ, int.coe_nat_dvd.mp], | |||
| refine (zmod.int_coe_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp _, | |||
| simp only [int.cast_pow, int.cast_add, int.cast_one, zmod.coe_val_min_abs], | |||
| rw hy, exact add_left_neg 1 }, | |||
| rw [pow_two, ← hy], exact add_left_neg 1 }, | |||
There was a problem hiding this comment.
What happened here? Why was this change necessary?
There was a problem hiding this comment.
This is because I replaced ∃ y : zmod p, y ^ 2 = -1 in the statement of zmod.exists_sq_eq_neg_one_iffwith is_square (-1 : zmod p), which unfolds to ∃ y : zmod p, (-1 : zmod p) = y * y, so we have to convert between y * y and y ^ 2 and also use the symmetric version of the equality.
| -/ | ||
|
|
||
| section general | ||
|
|
||
| /-- An odd natural number has residue `1` or `3` mod `4`-/ | ||
| lemma odd_mod_four {n : ℕ} (hn : n % 2 = 1) : n % 4 = 1 ∨ n % 4 = 3 := |
There was a problem hiding this comment.
This can be turned into an iff (or maybe we want both versions). As iff statement, it can be used in rw, which I guess will be useful.
There was a problem hiding this comment.
Makes sense; I'll change to odd_mod_four_iff. Should this go into the nat namespace?
There was a problem hiding this comment.
I've moved it into the nat namespace (where the partial converses also reside).
| simp only [nat.bit0_mod_two, zero_pow', ne.def, pnat.ne_zero, not_false_iff, nat.zero_mod], | ||
| end | ||
|
|
||
| /-- If the finite field `F` has characteristic `≠ 2`, then it has odd cardinality. -/ | ||
| lemma odd_card_of_char_ne_two (hF : ring_char F ≠ 2) : fintype.card F % 2 = 1 := | ||
| begin |
There was a problem hiding this comment.
It should be possible to golf this proof, using even_card_of_char_two above. It is the contrapositive + the fact that % 2 numbers are = 0 xor = 1.
There was a problem hiding this comment.
OK; I'll look into it. (The second proof was there before the first.)
There was a problem hiding this comment.
It is not really the contrapositive. I have now changed the first into an equivalence; then the two statements can easily be derived from that.
There was a problem hiding this comment.
(Or rather, added the iff version of the first...)
| map_zero' := rfl, map_one' := rfl, map_mul' := dec_trivial } | ||
|
|
||
| /-- An explicit description of `χ₄` on integers / naturals -/ | ||
| lemma χ₄_of_mod_four_int (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := |
There was a problem hiding this comment.
of suggests that the argument is an integer mod 4. The first thing that popped into my mind is:
| lemma χ₄_of_mod_four_int (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := | |
| lemma χ₄_int_eq_if_mod4 (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := |
But I guess there is room for improvement.
There was a problem hiding this comment.
χ₄_int_eq_if_mod_four seems to be more consistent with what is already there and talks about residues mod 4.
| exact help (n % 4) (int.mod_nonneg n (by norm_num)) (int.mod_lt n (by norm_num)), | ||
| end | ||
|
|
||
| lemma χ₄_of_mod_four_nat (n : ℕ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := |
There was a problem hiding this comment.
Then this would be
| lemma χ₄_of_mod_four_nat (n : ℕ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := | |
| lemma χ₄_nat_eq_if_mod4 (n : ℕ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := |
There was a problem hiding this comment.
..._if_mod_four as for the int version.
jcommelin
added
awaiting-author
MichaelStollBayreuth
removed
the
awaiting-author
MichaelStollBayreuth
added
the
awaiting-review
leanprover-community-bot-assistant
added
ready-to-merge
…3978) This PR adds code expressing the value of the quadratic character at -1 of a finite field of odd characteristic as χ₄ applied to the cardinality of the field. This is then also done for the Legendre symbol. Additional changes: * two helper lemmas `odd_mod_four` and `finite_field.even_card_of_char_two` that are needed * some API lemmas for χ₄ * write `euler_criterion` and `exists_sq_eq_neg_one_iff` in terms of `is_square`; simplify the proof of the latter using the general result for quadratic characters
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This PR adds code expressing the value of the quadratic character at -1 of a finite field of odd characteristic as χ₄ applied to the cardinality of the field. This is then also done for the Legendre symbol.
Additional changes:
odd_mod_fourandfinite_field.even_card_of_char_twothat are neededeuler_criterionandexists_sq_eq_neg_one_iffin terms ofis_square; simplify the proof of the latter using the general result for quadratic characters