mathlib3

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