OAI/Analysis/CharacterCriterion/TensorComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.Representations.gnsVector_norm_sq line 39
  2. lemma OAI.KirchbergRordam.Representations.gnsVector_unit_norm line 43
  3. lemma OAI.KirchbergRordam.Representations.gnsVector_norming_norm line 48
  4. lemma OAI.KirchbergRordam.MinTensor.RepresentationPair.tmul_norm line 57
  5. theorem OAI.KirchbergRordam.MinTensor.norm_tmul line 65
  6. lemma OAI.KirchbergRordam.MinTensor.includeLeft_isometry line 109
  7. lemma OAI.KirchbergRordam.MinTensor.includeRight_isometry line 115
  8. theorem OAI.KirchbergRordam.spatial_absorption_of_central_maximal_half_flip line 128
  9. theorem OAI.KirchbergRordam.balanced_drop_absorption line 227
  10. instance OAI.KirchbergRordam.MaxTensor.nontrivial_of_spatial line 241
  11. lemma OAI.KirchbergRordam.MaxTensor.includeLeft_isometry line 243