mathlib3
42388681 - chore(analysis): rename times_cont_diff (#12227)

Commit
4 years ago
chore(analysis): rename times_cont_diff (#12227) This replaces `times_cont_diff` by `cont_diff` everywhere, and the same for `times_cont_mdiff`. There is no change at all in content. See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/times_cont_diff.20name Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Author
Parents
Loading