OAI/RepresentationTheory/UniversalSquare/Specht/PieriInduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Pieri Induction.

  1. theorem OAI.Saxl.horizontal_placed_restriction line 17
  2. def OAI.Saxl.tensorTrivial line 27
  3. lemma OAI.Saxl.tensorTrivial_injective line 31
  4. theorem OAI.Saxl.horizontal_coind_map line 38
  5. theorem OAI.Saxl.Balance.even_twos_odd_coind line 71
  6. theorem OAI.Saxl.Balance.two_paths_two_coind line 95