OAI/Analysis/FreeWords/UnitaryTraceWitnessSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KKFactorSupport.gnsVector_mul_unitary_norm line 18
2. theorem OAI.KKFactorSupport.gnsVector_conj_sub_norm line 35