mathlib3
1a57c79e - feat(analysis/calculus): assorted simple lemmas (#10975)

Commit
4 years ago
feat(analysis/calculus): assorted simple lemmas (#10975) Various lemmas from the formalization of the Cauchy integral formula (#10000 and some later developments on top of it). Also add `@[measurability]` attrs to theorems like `measurable_fderiv`.
Author
Parents
Loading