mathlib

2b79f1da - feat(ring_theory/ideal_operations): lemmas about ideals and galois connections (#2767)