Commit 2025-09-03 14:38 a6bab243

View on Github →

feat(Ideal): relNorm is preserved under the action of an AlgEquiv (#28724) More precisely: for I : Ideal S and σ : S ≃ₐ[R] T, we have relNorm R (map σ I) = relNorm R I

Estimated changes

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

added theorem Ideal.relNorm_comap_algEquiv

added theorem Ideal.relNorm_map_algEquiv

added theorem Ideal.relNorm_smul

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

added theorem Algebra.intNorm_map_algEquiv

added def galLiftEquiv

added theorem galLiftEquiv_algebraMap_apply

added theorem galLift_id

added theorem galRestrict'_id

added theorem galRestrict_symm_algebraMap_apply