OAI/Analysis/KadisonKastler/SymmetricVectorAngle.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal decomposition of two symmetric unit vectors

  1. theorem OAI.KadisonKastler.conjugateIsometry_real_smul line 17
  2. theorem OAI.KadisonKastler.symmetric_inner_real line 23
  3. theorem OAI.KadisonKastler.symmetric_unit_angle_decomposition line 36
  4. theorem OAI.KadisonKastler.ModularConjugationData.noncollinear_projection_witness line 90