mathlib3

43cb3ffc - fix(ring_theory/ideal/operations): fix a name and dot notation (#12507)