OAI/Analysis/HyperbolicCones/BlockNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed positive-definite diagonal congruence makes both positive maps unital.

  1. def OAI.Paper256.RawBlockPencil.normalize line 13