chore(Mathlib/Tactic): stop norm_num importing the Bochner integral (#39602)

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.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: b-mehta

Mathlib.lean

@@ -5690,6 +5690,7 @@ public import Mathlib.NumberTheory.LSeries.ZMod
 public import Mathlib.NumberTheory.LSeries.ZetaZeros
 public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 public import Mathlib.NumberTheory.LegendreSymbol.Basic
+public import Mathlib.NumberTheory.LegendreSymbol.Complex
 public import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
 public import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
 public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

@@ -5,10 +5,10 @@ Authors: David Loeffler
 -/
 module
 
+public import Mathlib.Analysis.Complex.Polynomial.Basic
 public import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 public import Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
-public import Mathlib.Topology.Instances.AddCircle.Real
 
 /-!
 # Additive characters valued in the unit circle

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

@@ -9,7 +9,6 @@ public import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
 public import Mathlib.FieldTheory.Finite.Trace
 public import Mathlib.Algebra.Group.AddChar
 public import Mathlib.Data.ZMod.Units
-public import Mathlib.Analysis.Complex.Polynomial.Basic
 
 /-!
 # Additive characters of finite rings and fields
@@ -40,6 +39,7 @@ additive character
 
 @[expose] public section
 
+assert_not_exists MeasureTheory.integral
 
 universe u v
 
@@ -291,25 +291,4 @@ lemma starComp_apply (hR : 0 < ringChar R) {φ : AddChar R ℂ} (a : R) :
 
 end Ring
 
-section Field
-
-variable (F : Type*) [Field F] [Finite F]
-
-private lemma ringChar_ne : ringChar ℂ ≠ ringChar F := by
-  simpa only [ringChar.eq_zero] using (CharP.ringChar_ne_zero_of_finite F).symm
-
-/-- A primitive additive character on the finite field `F` with values in `ℂ`. -/
-noncomputable def FiniteField.primitiveChar_to_Complex : AddChar F ℂ := by
-  letI ch := primitiveChar F ℂ <| by exact ringChar_ne F
-  refine MonoidHom.compAddChar ?_ ch.char
-  exact (IsCyclotomicExtension.algEquiv {(ch.n : ℕ)} ℂ (CyclotomicField ch.n ℂ) ℂ).toMonoidHom
-
-lemma FiniteField.primitiveChar_to_Complex_isPrimitive :
-    (primitiveChar_to_Complex F).IsPrimitive := by
-  refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_
-  let nn := (primitiveChar F ℂ <| ringChar_ne F).n
-  exact (IsCyclotomicExtension.algEquiv {(nn : ℕ)} ℂ (CyclotomicField nn ℂ) ℂ).injective
-
-end Field
-
 end AddChar

Mathlib/NumberTheory/LegendreSymbol/Complex.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2022 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+module
+
+public import Mathlib.Analysis.Complex.Polynomial.Basic
+public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
+
+/-!
+# Additive characters on finite fields
+
+We construct a primitive additive character on a finite field `F` with values in `ℂ`.
+This file is kept separate from `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` to avoid
+importing the fundamental theorem of algebra and Bochner integral into that file.
+-/
+
+namespace AddChar
+
+section Field
+
+variable (F : Type*) [Field F] [Finite F]
+
+lemma ringChar_ne : ringChar ℂ ≠ ringChar F := by
+  simpa only [ringChar.eq_zero] using (CharP.ringChar_ne_zero_of_finite F).symm
+
+/-- A primitive additive character on the finite field `F` with values in `ℂ`. -/
+public noncomputable def FiniteField.primitiveChar_to_Complex : AddChar F ℂ := by
+  letI ch := primitiveChar F ℂ <| by exact ringChar_ne F
+  refine MonoidHom.compAddChar ?_ ch.char
+  exact (IsCyclotomicExtension.algEquiv {(ch.n : ℕ)} ℂ (CyclotomicField ch.n ℂ) ℂ).toMonoidHom
+
+public lemma FiniteField.primitiveChar_to_Complex_isPrimitive :
+    (primitiveChar_to_Complex F).IsPrimitive := by
+  refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_
+  let nn := (primitiveChar F ℂ <| ringChar_ne F).n
+  exact (IsCyclotomicExtension.algEquiv {(nn : ℕ)} ℂ (CyclotomicField nn ℂ) ℂ).injective
+
+end Field
+
+end AddChar