Commit 2023-11-16 07:03 52199f53

chore: replace IsLocalization.eq_iff_exists' by exists_of_eq (#8335) The other direction is a consequence of IsLocalization.map_units. Also do the same for LocalizationMap and IsLocalizedModule. This means we have one less fact to prove when constructing an IsLocalization (etc.) instance (thus many proofs are golfed), but once we construct it we still have access to the eq_iff_exists lemmas (without the prime) so the API doesn't get less powerful.