Commit 2025-12-23 19:14 b043044f

fix: definition of Rat.IsIntegralClosure.intEquiv (#33203) Rat.IsIntegralClosure.intEquiv R (formerly Rat.intEquiv) defined an isomorphism between an integral closure R of ℤ in ℚ abstractly using bijectivity. This turns out to be not very usable in light of the fact that this isomorphism can be constructed alternatively by composing RingOfIntegers.equiv and Rat.ringOfIntegersEquiv. This PR redefines as the composition to ensure compabitility. Namely, when specialising to R = 𝓞 ℚ we have that Rat.IsIntegralClosure.intEquiv (𝓞 ℚ) : 𝓞 ℚ ≃+* ℤ and Rat.ringOfIntegersEquiv define the same isomorphism.