Commit 2025-09-27 09:23 af353e32

View on Github →

feat(FieldTheory/Galois): normal basis theorem (#27390) from Formalizing Class Field Theory

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Algebra/Polynomial/Module/AEval.lean

added theorem Module.AEval'.X_pow_smul_of

added theorem Module.AEval.X_pow_smul_of

Created Mathlib/FieldTheory/Galois/NormalBasis.lean

added theorem IsGalois.normalBasis_apply

added theorem exists_linearIndependent_algEquiv_apply

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

added theorem span_flip_eq_top_iff_linearIndependent

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

Modified docs/references.bib