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.