Commit 2025-08-22 16:49 24eedffb

View on Github →

feat(RingTheory/Ideal): prove transitivity for the relative norm (#27152) Let R ⊆ S ⊆ T be a tower of rings and I : Ideal T, then relNorm R I = relNorm R (relNorm S I) Also, add the relNorm version of spanNorm_le_comap that was forgotten in a previous PR.

Estimated changes