Theorem Ideal.absNorm_eq_pow_inertiaDeg

Modification history

2025-05-15 10:23
Mathlib/NumberTheory/RamificationInertia/Basic.lean
feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc (#24706) …
Added Ideal.absNorm_eq_pow_inertiaDegView on Github →