Commit 2025-05-07 19:10 acc88736

View on Github →

feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver (#24381) We add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver, the standard formulation of Kummer's criterion to prove that the ring of integers of a number field is a principal ideal domain.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

added theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver_of_le

added theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le

added theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime