Zulip Chat Archive

Stream: Is there code for X?

Topic: measurable_space ℤˣ

Alex Kontorovich (Oct 26 2022 at 21:15):

I see we have measurable_space ℤ (int.measurable_space), but do we have measurable_space ℤˣ? Thanks!

Alex Kontorovich (Oct 26 2022 at 21:17):

I guess I can just add instance int.units.measurable_space : measurable_space ℤˣ := ⊤ ?

Anatole Dedecker (Oct 26 2022 at 21:18):

We should have it, because we have docs#units.measurable_space

Last updated: Dec 20 2023 at 11:08 UTC