Commit 2024-09-04 01:35 5bb23da7
View on Github →feat: the completion of a normed and completable topological field is a normed field (#15064)
This PR contains the result that the UniformSpace.Completion of a normed and completable topological field is also a normed field.
This has been split from the larger PR #13577.