2025-05-15 10:23
Mathlib/NumberTheory/NumberField/ClassNumber.lean
feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc (#24706) …
Modified RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime