OAI/Geometry/EinsteinFour/CP2NonorthogonalFixed.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An involution preserving projective transition probabilities fixes the central line of any nonorthogonal two-point orbit.

  1. theorem OAI.PositiveEinsteinFour.cp2_nonorthogonal_fixed line 14