OAI/InformationTheory/Entanglement/DefaultNull.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.PositiveMatrixMeasure.ext_entry_default line 13
2. lemma OAI.SecretKey.PositiveMatrixMeasure.value_zero_of_trace_zero line 18
3. lemma OAI.SecretKey.PositiveMatrixMeasure.traceMeasure_eq_zero_iff line 24
4. lemma OAI.SecretKey.PositiveMatrixMeasure.subevent_zero_of_trace_zero line 29
5. def OAI.SecretKey.PositiveMatrixMeasure.map line 36
6. lemma OAI.SecretKey.PositiveMatrixMeasure.map_value line 41
7. lemma OAI.SecretKey.PositiveMatrixMeasure.map_congr_trace_ae line 45
8. theorem OAI.SecretKey.PositiveMatrixMeasure.default_output_unchanged line 59