feat(NumberTheory/LegendreSymbol/QuadraticChar/Basic): characterize when products are squares

[bryan-hu]

Motivation

This is a basic application of the quadratic character of a finite field that can be used in many instances, for example later to characterize squares in ℤ_[p].

Summary

FiniteField.isSquare_mul_iff characterizes when the product of two nonzero elements in a finite field is a square, using the quadratic character.

Testing

• lake build Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic -q --log-level=info
• lake exe lint-style Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
• git diff --check upstream/master...HEAD

AI assistance

I was working with AI assistance (Claude Code, Codex) to formalize some fun number theory I like (Hilbert symbols, towards reciprocity laws) to help me learn Lean. I used AI assistance to highlight some small pieces that might be appropriate for mathlib, and to help me properly format these small items for mathlib.

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary cc714f1733

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ FiniteField.isSquare_mul_iff
+ FiniteField.isSquare_mul_of_not_isSquare_of_not_isSquare
+ FiniteField.not_isSquare_mul_of_isSquare_of_not_isSquare
+ FiniteField.not_isSquare_mul_of_not_isSquare_of_isSquare

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit cc714f1).

• +4 new declarations
• −0 removed declarations

+FiniteField.isSquare_mul_iff
+FiniteField.isSquare_mul_of_not_isSquare_of_not_isSquare
+FiniteField.not_isSquare_mul_of_isSquare_of_not_isSquare
+FiniteField.not_isSquare_mul_of_not_isSquare_of_isSquare

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit cc714f1733
Reference commit 3de5ed81cc

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[felixpernegger]

LLM-generated

[loefflerd]

This is a nice idea! I wasn't familiar with the cases nonempty_fintype idiom, but it seems to be quite common in this part of the library.

Just one suggestion to make it more potentially useful elsewhere: as well as the iff lemma IsSquare a ↔ IsSquare b, you could have more direct lemmas (complementing the existing IsSquare.mul) which assert that a * b is, or is not, a square assuming each of the possible combinations of a, b being squares / non-squares. This is not as concise as the formulation you have here, but would be easier to re-use later.

[bryan-hu]

@loefflerd thank you for the suggestion!

Besides adding a lemma that asserts a*b is a square in a finite field when a and b are both nonsquares, should we also add the other combinations here? I am asking because a*b being a nonsquare when a is a (nonzero) square and b is a nonsquare holds more generally.

[loefflerd]

Besides adding a lemma that asserts a*b is a square in a finite field when a and b are both nonsquares, should we also add the other combinations here? I am asking because a*b being a nonsquare when a is a (nonzero) square and b is a nonsquare holds more generally.

I think all three of the implications (other than the straightforward "a, b square => a*b square") require the base to be a field. For the implication (a square, b non-square) => (a * b non-square), with a, b non-zero, there is a counterexample in Z/6Z (take a= 3, b = 5, noting 3 = 3^2 mod 6). To get this implication to work in a general commutative ring you need to assume a, b are units, not just non-zero.

[bryan-hu]

Besides adding a lemma that asserts a*b is a square in a finite field when a and b are both nonsquares, should we also add the other combinations here? I am asking because a*b being a nonsquare when a is a (nonzero) square and b is a nonsquare holds more generally.

I think all three of the implications (other than the straightforward "a, b square => a*b square") require the base to be a field. For the implication (a square, b non-square) => (a * b non-square), with a, b non-zero, there is a counterexample in Z/6Z (take a= 3, b = 5, noting 3 = 3^2 mod 6). To get this implication to work in a general commutative ring you need to assume a, b are units, not just non-zero.

Yes, I meant that the a and b nonsquare => a*b square implication is the one piece that is specific to finite fields vs. any field

[loefflerd]

Yes, I meant that the a and b nonsquare => a*b square implication is the one piece that is specific to finite fields vs. any field

I see: you were thinking of non-finite fields, I was thinking of finite non-fields. A lemma asserting this (and its mirror-image twin) for general fields would indeed be useful.

[bryan-hu]

@loefflerd great, thank you!

I've added the other implications, except 'a' and 'b' square => 'a*b' square, which is IsSquare.mul I think.