OAI/Geometry/EinsteinFour/ComplexPairAlignment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unit representatives with nonnegative real overlap, including orthogonal pairs.

  1. theorem OAI.PositiveEinsteinFour.Geometry.cp2_aligned_unit_representative line 10