mathlib

778dfd50 - chore(analysis/locally_convex/basic): generalize lemmas and add simple lemmas (#12643)

chore(analysis/locally_convex/basic): generalize lemmas and add simple lemmas (#12643) Gerenalize all 'simple' lemmas for `absorb` and `absorbent` to the type-class `[semi_normed_ring 𝕜] [has_scalar 𝕜 E]`. Additionally, add the lemmas `absorbs_empty`, `balanced_mem` and `zero_singleton_balanced`.