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.