Commit 2025-11-05 09:57 241eb4c2

feat(DedekindDomain): lift a basis in a disjoint extension when the different ideals are coprime (#29885) Let A ⊆ B be a finite extension of Dedekind domains and assume that A ⊆ R₁, R₂ ⊆ B are two subrings such that Frac R₁ ⊔ Frac R₂ = Frac B, Frac R₁ and Frac R₂ are linearly disjoint over Frac A, and that 𝓓(R₁/A) and 𝓓(R₂/A) are coprime where 𝓓 denotes the different ideal and Frac R denotes the fraction field of a domain R. This PR constructs a R₁-basis of B by lifting an A-basis of R₂.