OAI/RepresentationTheory/UniversalSquare/Specht/ColumnRestriction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Column Restriction.

  1. def OAI.Saxl.FlagColumns.coordinateFlag line 19
  2. lemma OAI.Saxl.FlagColumns.wedge_coordinateFlag line 22
  3. lemma OAI.Saxl.FlagColumns.column_split_basis_nonzero line 46
  4. theorem OAI.Saxl.FlagColumns.split_blocks_nonzero line 76
  5. def OAI.Saxl.FlagColumns.placedFlagMap line 94
  6. lemma OAI.Saxl.FlagColumns.placed_blocks_in_range line 101
  7. lemma OAI.Saxl.FlagColumns.product_in_external_range line 109
  8. lemma OAI.Saxl.FlagColumns.external_range_restriction_support line 122
  9. lemma OAI.Saxl.FlagColumns.placed_pair_support line 139
  10. theorem OAI.Saxl.FlagColumns.column_split_restriction line 151