OAI/Analysis/HyperbolicCones/MatrixResolvent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.isUnit_of_adjoint_difference_posDef line 12
2. theorem OAI.Paper256.resolvent_adjoint_difference line 28
3. theorem OAI.Paper256.positive_map_resolvent_isUnit line 49