Skip to content

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

Draft
lowasser wants to merge 34 commits into
UniMath:masterfrom
lowasser:cauchy-reals
Draft

The metric abelian group formed by the metric quotient of the Cauchy pseudocompletion of a pseudometric group#1985
lowasser wants to merge 34 commits into
UniMath:masterfrom
lowasser:cauchy-reals

Conversation

@lowasser

Copy link
Copy Markdown
Collaborator

This only constructs the abelian group so far; I still need to show addition and negation are isometries, but I don't anticipate that being difficult.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant