mathlib3

7e5ac6ad - chore(analysis/convex/strict): Reduce typeclass assumptions, golf (#12627)

chore(analysis/convex/strict): Reduce typeclass assumptions, golf (#12627) Move lemmas around so they are stated with the correct generality. Restate theorems using pointwise operations. Golf proofs. Fix typos in docstrings.