Commit 2025-08-16 16:09 c0a057e4
View on Github →feat(Algebra/intNorm): x divides intNorm x (#28021)
The main result of this PR is that x ∣ algebraMap A B (intNorm A B x).
From this we deduce that, for an ideal I, we have
spanNorm R I ≤ comap (algebraMap R S) I.