Commit 2023-01-13 22:32 c3350dbc

feat(ring_theory): equality of ideals from locally at each maximal ideal (#18142) This PR shows that an ideal is equal to another if all localizations at each maximal ideal are equal, by showing an ideal is included in another if this holds locally at each maximal ideal. This generalizes ideal_eq_zero_of_localization. The proof is inspired somewhat by the one for maximal_spectrum.infi_localization_eq_bot, although I couldn't find out a neat way to prove it from the new results since it talks about slightly different maps. It would also require readjusting the imports. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Equality.20of.20ideals.20from.20local.20equality