Commit 2025-10-24 05:21 be9d1e42

feat(DedekindDomain): formulas for the different ideal in the compositum of disjoint extensions (#29770) Let A ⊆ B be a finite extension of Dedekind domains and assume that A ⊆ R₁, R₂ ⊆ B are two subrings such that R₁ ⊔ R₂ = B, their fractions fields are linearly disjoint (over the fraction field of A) and that 𝓓(R₁/A) and 𝓓(R₂/A) are coprime, where 𝓓 denote the different ideal. We prove in particular: 𝓓(B/A) = 𝓓(R₁/A) * 𝓓(R₂/A)