Commit 2025-09-22 16:24 7f8d282e

feat(Ring/DedekindDomain): formula for the splitting of prime ideals in an extension (#27105) This PR just puts together all the results that were already there to deduce:

 map (algebraMap S R) p = ∏ P ∈ p.primesOver R, P ^ p.ramificationIdx (algebraMap S R) P

for p a maximal ideal of a ring S and R an extension of S that is a Dedekind ring. Note. There is a significant import increase in the file RingTheory.DedekindDomain.Factorization. However, this file is almost a leaf file so this increase only affects a limited number of files. If the increase is too big, a new file, say RingTheory.DedekindDomain.PrimeSplitting, can be added instead.