Theorem Algebra.intNorm_intNorm

Modification history

2025-08-22 16:49
Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
feat(RingTheory/Ideal): prove transitivity for the relative norm (#27152) …
Added Algebra.intNorm_intNormView on Github →