Commit 2025-10-12 17:44 417cda33

View on Github →

feat: remove separability assumption from Algebra.norm_eq_norm_adjoin and Algebra.norm_eq_prod_roots (#30448) Continuing the work of #30323 we remove the separability assumption from Algebra.norm_eq_norm_adjoin and Algebra.norm_eq_prod_roots.

Estimated changes

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Norm.lean

modified theorem RingOfIntegers.dvd_norm

modified theorem RingOfIntegers.isUnit_norm_of_isGalois

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/Norm/Basic.lean

deleted theorem Algebra.norm_eq_norm_adjoin

deleted theorem Algebra.norm_eq_prod_automorphisms

deleted theorem Algebra.norm_eq_prod_embeddings

deleted theorem Algebra.norm_eq_prod_roots

Modified Mathlib/RingTheory/Norm/Transitivity.lean

modified theorem Algebra.isIntegral_norm

added theorem Algebra.norm_eq_norm_adjoin

added theorem Algebra.norm_eq_prod_automorphisms

added theorem Algebra.norm_eq_prod_embeddings

added theorem Algebra.norm_eq_prod_roots