Commit 2026-05-25 21:53 0a24ddb8
View on Github →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.