mathlib3

feat(algebra/*): morphisms from closures are equal if they agree on generators

#18836

Open