Zulip Chat Archive
Stream: condensed mathematics
Topic: SemiNormedGroup_Completion.lean
Riccardo Brasca (Oct 18 2021 at 11:20):
I am going to open a PR to have for_mathlib/SemiNormedGroup_Completion in mathlib. I created the file but I am not the original author (git blame and github history only show me and Johan as authors), and I don't remember who wrote it in the first place. If you want to be mentioned in the authors list let me know.
Riccardo Brasca (Oct 18 2021 at 11:41):
Patrick Massot (Oct 18 2021 at 11:52):
You shouldn't need to come back to things like completion.induction_on₂. It means that either some lemmas are missing in mathlib or their use is missing in LTE.
Patrick Massot (Oct 18 2021 at 11:52):
I'll try to fix this soonish. Could you please tag the PR as WIP and ping me if I forget to work on it?
Riccardo Brasca (Oct 18 2021 at 11:54):
OK!
Riccardo Brasca (Oct 18 2021 at 11:56):
Indeed this can probably be golfed a lot using the results in analysis.normed.group.hom_completion. Let me see what I can do.
Riccardo Brasca (Oct 18 2021 at 12:58):
It seems that the only missing thing in analysis.normed.group.hom_completion is the extension to the completion of a morphism with complete codomain. I am working on it.
Riccardo Brasca (Oct 18 2021 at 13:51):
It should be ready for review now.
Patrick Massot (Oct 18 2021 at 14:18):
Indeed it looks much better now
Patrick Massot (Oct 18 2021 at 14:27):
I reviewed it.
Last updated: Dec 20 2023 at 11:08 UTC