mathlib

b21c1c9b - split(analysis/locally_convex/basic): Split off `analysis.seminorm` (#12624)

split(analysis/locally_convex/basic): Split off `analysis.seminorm` (#12624) Move `balanced`, `absorbs`, `absorbent` to a new file. For `analysis.seminorm`, I'm crediting * Jean for #4827 * myself for * #9097 * #11487 * Moritz for * #11329 * #11414 * #11477 For `analysis.locally_convex.basic`, I'm crediting * Jean for #4827 * Bhavik for * #7358 * #9097 * myself for * #9097 * #10999 * #11487