OAI/RepresentationTheory/UniversalSquare/Balance/WordPackingGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Word Packing Geometry.

  1. theorem OAI.Saxl.Balance.WordPacking.of_bounded_shape line 16
  2. theorem OAI.Saxl.Balance.WordPacking.neighbor line 27
  3. lemma OAI.Saxl.Balance.replicate_sorted line 46
  4. lemma OAI.Saxl.Balance.repeated_column_length line 49
  5. theorem OAI.Saxl.Balance.WordPacking.repeated line 62