feat(FieldTheory/Galois): normal basis theorem

[alreadydone]

To be cleaned up

Co-authored-by: Madison Crim @maddycrim
Co-authored-by: Aaron Liu @plp127
Co-authored-by: Justus Springer @justus-springer

from Formalizing Class Field Theory

---

• depends on: feat(Algebra): annihilator of fg module over PID is ann of some element #27355
• depends on: feat(FieldTheory/Finite): minimal polynomial of Frobenius #27368

[github-actions]

PR summary 9951132ce3

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Ideal.Maps	1073	1075	+2 (+0.19%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.Monoidal	1
123 files Mathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.CubicDiscriminant Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Star.Unitary Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Data.ZMod.Coprime Mathlib.FieldTheory.RatFunc.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.LinearAlgebra.TensorProduct.Quotient Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.NumberTheory.Dioph Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.FLT.MasonStothers Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.ValuativeRel Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.PythagoreanTriples Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.RingTheory.AdicCompletion.Basic Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.Bezout Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.DividedPowers.SubDPIdeal Mathlib.RingTheory.DualNumber Mathlib.RingTheory.EisensteinCriterion Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Finiteness.Ideal Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Ideal.AssociatedPrime.Basic Mathlib.RingTheory.Ideal.AssociatedPrime.Localization Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.MinimalPrime.Localization Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Ideal.Quotient.Operations Mathlib.RingTheory.Ideal.Quotient.PowTransition Mathlib.RingTheory.Idempotents Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.Jacobson.Ideal Mathlib.RingTheory.Jacobson.Radical Mathlib.RingTheory.Lasker Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.LocalSubring Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.NonLocalRing Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.Localization.Ideal Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Nakayama Mathlib.RingTheory.Polynomial.ContentIdeal Mathlib.RingTheory.Polynomial.Content Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.RingTheory.Polynomial.Eisenstein.Criterion Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished Mathlib.RingTheory.Polynomial.Eisenstein.Generalized Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.Radical Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.SimpleRing.Matrix Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.TensorProduct.Quotient Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.Quotient Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Valuation.ValuativeRel Mathlib.Topology.Algebra.IsOpenUnits Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Star.Unitary Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.Sheaves.CommRingCat	2
Mathlib.FieldTheory.Galois.NormalBasis (new file)	1942

---

Declarations diff

+ AEval'.X_pow_smul_of
+ Module.annihilator_dfinsupp
+ Module.annihilator_finsupp
+ Module.annihilator_pi
+ Module.annihilator_prod
+ X_pow_smul_of
+ exists_ker_toSpanSingleton_eq_annihilator
+ exists_linearIndependent_algEquiv_apply
+ minpoly_frobeniusAlgHom
+ normalBasis
+ normalBasis_apply
+ span_flip_eq_top_iff_linearIndependent
+ toAlgHomHom
+ toEnd

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.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
820	1	erw

Current commit 4143b8e4cf
Reference commit 9951132ce3

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra): annihilator of fg module over PID is ann of some element #27355
• feat(FieldTheory/Finite): minimal polynomial of Frobenius #27368
  By Dependent Issues (🤖). Happy coding!