Commit 2025-10-09 08:14 1ed2babe

View on Github →

feat: remove separability assumption from Algebra.isIntegral_norm (#30323) We generalize Algebra.isIntegral_norm removing the assumption that L/K is separable.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Norm.lean

modified theorem RingOfIntegers.algebraMap_norm_algebraMap

modified theorem RingOfIntegers.coe_algebraMap_norm

modified theorem RingOfIntegers.coe_norm

modified theorem RingOfIntegers.norm_algebraMap

modified theorem RingOfIntegers.norm_norm

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

modified theorem Ideal.relNorm_le_comap

modified theorem Ideal.spanNorm_le_comap

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

modified def Algebra.intNormAux

modified theorem Algebra.map_intNormAux

Modified Mathlib/RingTheory/Norm/Basic.lean

deleted theorem Algebra.isIntegral_norm

Modified Mathlib/RingTheory/Norm/Transitivity.lean

added theorem Algebra.isIntegral_norm

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean