The proof (instantiation) that the complex-linear bounded operators (type complex_bounded) are a complex Banach space (type cbanach) is complete. Good news for automated reasoning :robot: about infinitely many degrees of freedom :atom:
Last updated: Sep 16 2025 at 12:42 UTC