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: May 02 2025 at 03:31 UTC