OAI/RepresentationTheory/UniversalSquare/Specht/NoMixedColumns.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

No Mixed Columns.

  1. lemma OAI.Saxl.FlagColumns.wedge_apply_det line 17
  2. theorem OAI.Saxl.FlagColumns.wedge_split_of_zero line 24
  3. def OAI.Saxl.FlagColumns.joinedFlag line 49
  4. lemma OAI.Saxl.FlagColumns.joinedFlag_left line 52
  5. lemma OAI.Saxl.FlagColumns.joinedFlag_right line 55
  6. theorem OAI.Saxl.FlagColumns.joinedFlag_column_factor line 59
  7. def OAI.Saxl.FlagColumns.clearSlots line 77
  8. theorem OAI.Saxl.FlagColumns.blocks_factor_of_clearSlots line 85
  9. theorem OAI.Saxl.FlagColumns.blocks_pair_factor_of_clearSlots line 108
  10. lemma OAI.Saxl.FlagColumns.blocks_alphabet line 123
  11. theorem OAI.Saxl.FlagColumns.band_contraction_factor line 135