Commit 2020-04-26 06:46 401d3216

feat(analysis/normed_space/basic): add continuous_at.div (#2532) When proving a particular function continuous at a particular point, lemmas such as continuous_at.mul, continuous_at.add and continuous_at.comp can be used to build this up from continuity properties of simpler functions. It's convenient to have something similar for division as well. This adds continuous_at.div for normed fields, as suggested by Yury. If mathlib gets topological (semi)fields in future, this should become a result for those.