Commit 2022-03-17 06:22 7000efb8
View on Github →refactor(analysis/specific_limits): split into two files (#12759)
Split the 1200-line file analysis.specific_limits
into two:
analysis.specific_limits.normed
importsnormed_space
and covers limits in normed rings/fieldsanalysis.specific_limits.basic
imports only topology, and is still a bit of a grab-bag, covering limits in metric spaces, ordered rings,ennreal
, etc.