Theorem IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply

Modification history

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