mathlib3

15da6257 - chore(analysis/locally_convex): golf a proof (#15323)