src/HOL/Library/Complex_Order.thy
Wed, 06 Oct 2021 14:19:46 +0200 eberlm new notion of infinite sums in HOL-Analysis, ordering on complex numbers
less more (0) tip