The metric abelian group formed by the metric quotient of the Cauchy pseudocompletion of a pseudometric group

config/codespell-ignore.txt

@@ -1,3 +1,4 @@
+Nd
 Tim
 blacklist
 couldn

src/analysis.lagda.md

@@ -3,13 +3,20 @@
 ```agda
 module analysis where
 
+open import analysis.abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups public
+open import analysis.addition-cauchy-approximations-metric-abelian-groups public
 open import analysis.alternation-sequences-metric-abelian-groups public
+open import analysis.cauchy-approximations-metric-abelian-groups public
+open import analysis.cauchy-pseudocompletions-metric-abelian-groups public
 open import analysis.complete-metric-abelian-groups public
 open import analysis.convergent-series-complete-metric-abelian-groups public
 open import analysis.convergent-series-metric-abelian-groups public
 open import analysis.limits-of-sequences-metric-abelian-groups public
 open import analysis.metric-abelian-groups public
+open import analysis.metric-abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups public
 open import analysis.metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups public
+open import analysis.metric-quotients-cauchy-pseudocompletions-metric-abelian-groups public
+open import analysis.negation-cauchy-approximations-metric-abelian-groups public
 open import analysis.sequences-metric-abelian-groups public
 open import analysis.series-complete-metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public