Stream: condensed mathematics
Topic: profinite trivialities
Johan Commelin (Apr 10 2021 at 05:45):
Pow which takes powers of profinite sets.
- We'll need
Pow_mul'which give functorial isos .
- Do we already have
Adam Topaz (Apr 10 2021 at 13:06):
In the cech_stuff branch, I added iso_of_bijective :wink:
Last updated: May 09 2021 at 16:20 UTC