mathlib3

75e7fca5 - feat(analysis/calculus/mean_value): functions are equal if their derivatives and a point are equal (#19059)

feat(analysis/calculus/mean_value): functions are equal if their derivatives and a point are equal (#19059) And the version for equality within a convex set. Co-authored-by: ADedecker <anatolededecker@gmail.com>