OAI/Probability/BinarySweep/YoungTheory/CutTensor.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Young.tensor_map_injective_complex line 13
  2. abbrev OAI.BinaryCoordinateSweeps.Young.CutTensor line 25
  3. abbrev OAI.BinaryCoordinateSweeps.Young.CutTabloids line 26
  4. def OAI.BinaryCoordinateSweeps.Young.cutTensorInclude line 28
  5. lemma OAI.BinaryCoordinateSweeps.Young.cutTensorInclude_tmul line 37
  6. lemma OAI.BinaryCoordinateSweeps.Young.cutTensorInclude_injective line 42
  7. def OAI.BinaryCoordinateSweeps.Young.cutRestriction line 63
  8. lemma OAI.BinaryCoordinateSweeps.Young.cutRestriction_poly line 68
  9. lemma OAI.BinaryCoordinateSweeps.Young.cutRestriction_translate line 75
  10. lemma OAI.BinaryCoordinateSweeps.Young.cut_tensor_orbit_mem_range line 88
  11. lemma OAI.BinaryCoordinateSweeps.Young.spechtPoly_span_top line 94
  12. lemma OAI.BinaryCoordinateSweeps.Young.cut_tensor_tmul_mem_range line 98
  13. theorem OAI.BinaryCoordinateSweeps.Young.cutTensor_range_le line 121
  14. def OAI.BinaryCoordinateSweeps.Irrep.averageLinear line 142
  15. lemma OAI.BinaryCoordinateSweeps.Irrep.averageLinear_apply line 145
  16. lemma OAI.BinaryCoordinateSweeps.Irrep.averageLinear_intertwines line 149
  17. def OAI.BinaryCoordinateSweeps.Irrep.averagedIntertwiner line 160
  18. lemma OAI.BinaryCoordinateSweeps.Irrep.averageLinear_lift line 164
  19. theorem OAI.BinaryCoordinateSweeps.Irrep.lift_intertwiner line 173