OAI/Geometry/EinsteinFour/CP2PairUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The unique top line of the sum of two nonorthogonal rank-one projections. Only this two-vector specialization is needed for the CP2 involution argument.

  1. theorem OAI.PositiveEinsteinFour.cp2_aligned_pair_data line 14
  2. theorem OAI.PositiveEinsteinFour.cp2_aligned_pair_top_unique line 31