From 6e844be9f6bdba7c66b2685000326c81065e2bbf Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 20 May 2026 02:49:08 +0100 Subject: [PATCH 1/8] chore(Mathlib/Tactic): stop norm_num importing the Bochner integral --- .../Complex/CircleAddChar.lean | 1 + .../LegendreSymbol/AddCharacter.lean | 22 ------------------- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean index 0d93d862f1370d..34548a1c63a76f 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean @@ -9,6 +9,7 @@ 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 +public import Mathlib.NumberTheory.LegendreSymbol.Cyclotomic /-! # Additive characters valued in the unit circle diff --git a/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean b/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean index 70752949df7f28..3c91df023fba2d 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean +++ b/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 @@ -291,25 +290,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 From ef6aaa94b55be7beeaedf01f7a3d64ae227873aa Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 20 May 2026 02:49:56 +0100 Subject: [PATCH 2/8] oops --- .../LegendreSymbol/Cyclotomic.lean | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean diff --git a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean b/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean new file mode 100644 index 00000000000000..687baa7933d681 --- /dev/null +++ b/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean @@ -0,0 +1,38 @@ +/- +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.NumberTheory.Cyclotomic.PrimitiveRoots +public import Mathlib.FieldTheory.Finite.Trace +public import Mathlib.Algebra.Group.AddChar +public import Mathlib.Data.ZMod.Units +public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter +public import Mathlib.Analysis.Complex.Polynomial.Basic + +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 `ℂ`. -/ +@[expose] 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 From c6776c8e8728e24d65e1bf092593239d34b259f4 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 20 May 2026 02:52:09 +0100 Subject: [PATCH 3/8] make it not weird --- Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean b/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean index 687baa7933d681..38b9c4931205ef 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean @@ -5,10 +5,6 @@ Authors: Michael Stoll -/ module -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.NumberTheory.LegendreSymbol.AddCharacter public import Mathlib.Analysis.Complex.Polynomial.Basic From 68dd1faad5fa5c42a26e28550c8043259809e475 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 20 May 2026 03:12:57 +0100 Subject: [PATCH 4/8] mk all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index dc75a5ae6400e0..14b877cb81f494 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5659,6 +5659,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.Cyclotomic public import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas public import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic From 4760b45047d672c1bc9ac09e80f3f030c18a559f Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Mon, 25 May 2026 18:24:39 +0100 Subject: [PATCH 5/8] add module doc --- Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean b/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean index 38b9c4931205ef..b2e7f7cf552f8e 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean @@ -5,8 +5,16 @@ Authors: Michael Stoll -/ module -public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter 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 From 0b96e6bcaabf0b23ee71f8a004a39939eebfaa55 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Mon, 25 May 2026 18:24:54 +0100 Subject: [PATCH 6/8] add assert_not_exists to prevent future regression --- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean b/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean index 3c91df023fba2d..f4c640a472ffb8 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean @@ -39,6 +39,7 @@ additive character @[expose] public section +assert_not_exists MeasureTheory.integral universe u v From 3f8be6e42f51ebd15c32a252d0bd291019fee176 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Mon, 25 May 2026 18:25:13 +0100 Subject: [PATCH 7/8] fix imports --- Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean index 34548a1c63a76f..4f8e207c7027df 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean @@ -5,11 +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 -public import Mathlib.NumberTheory.LegendreSymbol.Cyclotomic /-! # Additive characters valued in the unit circle From 41c067a2d506205d809c2d1119d04825cc407ada Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Mon, 25 May 2026 19:04:33 +0100 Subject: [PATCH 8/8] move file per MSB's suggestion --- Mathlib.lean | 2 +- .../LegendreSymbol/{Cyclotomic.lean => Complex.lean} | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename Mathlib/NumberTheory/LegendreSymbol/{Cyclotomic.lean => Complex.lean} (93%) diff --git a/Mathlib.lean b/Mathlib.lean index c13c7170a09467..15e1a4d0b2842c 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5686,7 +5686,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.Cyclotomic +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 diff --git a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean b/Mathlib/NumberTheory/LegendreSymbol/Complex.lean similarity index 93% rename from Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean rename to Mathlib/NumberTheory/LegendreSymbol/Complex.lean index b2e7f7cf552f8e..dbcd67af21572d 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/Cyclotomic.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/Complex.lean @@ -26,7 +26,7 @@ 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 `ℂ`. -/ -@[expose] public noncomputable def FiniteField.primitiveChar_to_Complex : AddChar F ℂ := by +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