[Merged by Bors] - chore(Mathlib/Tactic): stop norm_num importing the Bochner integral

[b-mehta]

Motivation: importing Mathlib.Tactic.NormNum shouldn't require us to build the Bochner integral and fundamental theorem of algebra.

To enable this, we move FiniteField.primitiveChar_to_Complex to a new file.
We also make FiniteField.primitiveChar_to_Complex not exposed, since its definitional properties should not be relied upon.

---

[b-mehta]

!radar

[leanprover-radar]

Benchmark results for c6776c8 against 260979c are in. No significant results found. @b-mehta

• 🟥 build//instructions: +45.7G (+0.03%)

Small changes (5✅)

• ✅ build/module/Mathlib.Lean.Name//instructions: -172.6M (-5.22%)
• ✅ build/module/Mathlib.NumberTheory.JacobiSum.Basic//instructions: -656.9M (-2.09%)
• ✅ build/module/Mathlib.NumberTheory.LegendreSymbol.AddCharacter//instructions: -1.4G (-7.38%)
• ✅ build/module/Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum//instructions: -547.5M (-4.16%)
• ✅ build/module/Mathlib.Tactic//instructions: -470.9M (-6.38%)

[github-actions]

PR summary 41c067a2d5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.LegendreSymbol.AddCharacter	3025	2608	-417 (-13.79%)

Import changes for all files

Files	Import difference
10 files Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.Tactic.NormNum.LegendreSymbol	-417
Mathlib.Tactic	-393
Mathlib.NumberTheory.LegendreSymbol.Complex (new file)	3026

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[b-mehta]

!radar

[leanprover-radar]

Benchmark results for 68dd1fa against 260979c are in. No significant results found. @b-mehta

• 🟥 build//instructions: +38.7G (+0.02%)

Small changes (4✅, 1🟥)

• ✅ build/module/Mathlib.NumberTheory.JacobiSum.Basic//instructions: -598.1M (-1.91%)
• ✅ build/module/Mathlib.NumberTheory.LegendreSymbol.AddCharacter//instructions: -1.4G (-7.51%)
• ✅ build/module/Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum//instructions: -546.9M (-4.15%)
• ✅ build/module/Mathlib.Tactic//instructions: -473.3M (-6.41%)
• 🟥 build/profile/import//wall-clock: +1m 46s (+1.54%)

[grunweg]

@adomani The module doc-string linter does not fire on this PR in CI.
It should fire here (the newly added module has no module doc-string); it does fire locally in VS Code --- but lake build passes locally and in CI. Do you have any idea what's causing this?

[grunweg]

On current master, the linter works: removing the module doc-string in an existing file (WhitneyEmbedding.lean) causes a linter error both in VS Code and in lake build.

[grunweg]

Basically LGTM --- but we should investigate the linter bug!

[grunweg]

The linter also errors in lake build if I copy-paste literally the same file on current master. Can you merge master on this PR?

[grunweg]

Merging master on this PR fixes the linter: this is the diff between the two points:
260979c...master

[adomani]

Some part of this linter relies on an IO.Ref and therefore may produce unreliable results locally. I think that I had aimed to making it silent, when it is unreliable.

In CI, though, the warnings should be correct. So I'm surprised that CI passed when it shouldn't.

[b-mehta]

@MichaelStollBayreuth if you have a moment, I'd also like your opinion on the new location for the definition, and the module doc. On hindsight, I'm not sure that Cyclotomic.lean really makes sense here.
Also, this could be a good opportunity to un-expose this definition, as I think the idea is that it's not meant to have good definitional properties, other than being a primitive character on a finite field.

[MichaelStollBayreuth]

• A separate file definitely makes sense. Maybe "Mathlib.NumberTheory.LegendreSymbol.Complex"?
• The module docstring looks OK to me.
• Un-exposeing the definition is fine as far as I am concerned. I agree that it should not matter how the character is constructed (one can obtain one from any other by pre-composing with multiplication by a unit), which, I assume, involves choice anyway somewhere (when picking a primitive pth root of unity).

[grunweg]

Thanks for doing this! This PR looks good to me. I'll let @MichaelStollBayreuth take a final look, as they wrote the code.
bors d=MichaelStollBayreuth

[mathlib-bors]

✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[MichaelStollBayreuth]

Thanks!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job