Theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le

Modification history

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_leView on Github →
2025-05-07 19:10
Mathlib/NumberTheory/NumberField/ClassNumber.lean
feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver (#24381) …
Added RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_leView on Github →