[Merged by Bors] - chore: split FieldTheory/IntermediateField

[kim-em]

---

[github-actions]

PR summary 3d1e3cc51a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.CharP.IntermediateField	1231	1007	-224 (-18.20%)
Mathlib.Topology.Instances.Complex	1471	1403	-68 (-4.62%)
Mathlib.FieldTheory.SplittingField.IsSplittingField	1242	1232	-10 (-0.81%)
Mathlib.RingTheory.LittleWedderburn	1667	1664	-3 (-0.18%)
Mathlib.LinearAlgebra.JordanChevalley	1269	1268	-1 (-0.08%)

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.IntermediateField	-1230
Mathlib.Algebra.CharP.IntermediateField	-224
Mathlib.Topology.Instances.Complex	-68
12 files Mathlib.RingTheory.IsAdjoinRoot Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.FieldTheory.Perfect Mathlib.NumberTheory.KummerDedekind Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.PerfectClosure Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.FieldTheory.SplittingField.Construction Mathlib.RingTheory.Perfection	-10
9 files Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Identities Mathlib.LinearAlgebra.Semisimple Mathlib.RingTheory.WittVector.Frobenius Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.NumberTheory.PrimesCongruentOne Mathlib.RingTheory.WittVector.DiscreteValuationRing	-4
Mathlib.RingTheory.LittleWedderburn	-3
Mathlib.LinearAlgebra.JordanChevalley	-1
106 files Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.FieldTheory.IsPerfectClosure Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.FieldTheory.Finite.Trace Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.GaussSum Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.RingTheory.Localization.NormTrace Mathlib.FieldTheory.AbelRuffini Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.NumberTheory.NumberField.Norm Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.FieldTheory.Galois Mathlib.RingTheory.Trace.Basic Mathlib.FieldTheory.Normal Mathlib.FieldTheory.Adjoin Mathlib.NumberTheory.NumberField.Discriminant Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Algebra.Lie.Derivation.Killing Mathlib.FieldTheory.SeparableClosure Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.Analysis.Fourier.ZMod Mathlib.NumberTheory.Cyclotomic.Three Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.RingTheory.Nullstellensatz Mathlib.FieldTheory.Fixed Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.Algebra.Lie.TraceForm Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.FieldTheory.Extension Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.RepresentationTheory.Invariants Mathlib.FieldTheory.KrullTopology Mathlib.CategoryTheory.Preadditive.Schur Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.FieldTheory.Finite.GaloisField Mathlib.RepresentationTheory.Character Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.Algebra.Lie.Weights.Chain Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.FieldTheory.PrimitiveElement Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.Analysis.Normed.Algebra.Basic Mathlib.RepresentationTheory.FDRep Mathlib.RingTheory.WittVector.Isocrystal Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Polynomial.Selmer Mathlib.FieldTheory.NormalClosure Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.Algebra.Lie.Weights.Killing Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.FieldTheory.KummerExtension Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.RingTheory.Ideal.Norm Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.FieldTheory.PurelyInseparable Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Analysis.CStarAlgebra.Module Mathlib.Tactic Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.RingTheory.Norm.Basic Mathlib.NumberTheory.FunctionField	1
Mathlib.FieldTheory.IntermediateField.Basic	902
Mathlib.FieldTheory.IntermediateField.Algebraic	1231

---

Declarations diff

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

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Ruben-VandeVelde]

lgtm

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style