mathlib3

c3350dbc - feat(ring_theory): equality of ideals from locally at each maximal ideal (#18142)

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 Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>