Zulip Chat Archive
Stream: general
Topic: set.compl
Kevin Buzzard (Jul 09 2020 at 12:25):
I just bumped the real number game to current mathlib, and there's no longer a has_neg instance on set X. Is there now notation for set.compl?
Ruben Van de Velde (Jul 09 2020 at 12:26):
Yeah, X^c since #3212
Kevin Buzzard (Jul 09 2020 at 12:27):
Thanks
Last updated: Dec 20 2023 at 11:08 UTC