Theorem IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count

Modification history

2025-09-22 16:24
Mathlib/RingTheory/DedekindDomain/Factorization.lean
feat(Ring/DedekindDomain): formula for the splitting of prime ideals in an extension (#27105) …
Added IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_countView on Github →