mathlib

434a938b - feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794)

feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794) Define `strictly_convex_space`, a `Prop`-valued mixin to state that a normed space is strictly convex. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>