OAI/Geometry/EinsteinFour/CP2OddOrthogonality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The odd-dimensional linear obstruction to an involution sending every complex projective line to an orthogonal line.

  1. theorem OAI.PositiveEinsteinFour.cp2_odd_orthogonality_obstruction line 15