Commit 2025-05-15 10:23 413d2060

feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc (#24706) We improve the statement of RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver_of_le to RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc: it is enough to only test primes p and ideals P such that p ^ ((span {p}).inertiaDeg P is less than Minkowski's bound. We also improve the structure of the file.