OAI/Analysis/Cotype/PatternProjections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.rowProjection line 10
  2. theorem OAI.Cotype.rowProjection_oddPart line 13
  3. theorem OAI.Cotype.row_twist_change line 29
  4. theorem OAI.Cotype.sign_coordinate_odd line 44
  5. theorem OAI.Cotype.matrixTwist_row_projection line 50
  6. def OAI.Cotype.columnProjection line 93
  7. theorem OAI.Cotype.columnProjection_oddPart line 96
  8. theorem OAI.Cotype.matrixTwist_transpose_swap line 100
  9. theorem OAI.Cotype.matrixTwist_column_projection line 111