OAI/Probability/BinarySweep/YoungTheory/CoinductionTools.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Irrep.toCoind line 18
  2. def OAI.BinaryCoordinateSweeps.Irrep.fromCoind line 32
  3. def OAI.BinaryCoordinateSweeps.Irrep.coindHomEquiv line 46
  4. lemma OAI.BinaryCoordinateSweeps.Irrep.multiplicity_symm line 61
  5. def OAI.BinaryCoordinateSweeps.Irrep.coindEvaluation line 75
  6. lemma OAI.BinaryCoordinateSweeps.Irrep.coindEvaluation_injective line 81
  7. lemma OAI.BinaryCoordinateSweeps.Irrep.coind_finrank_le line 92
  8. def OAI.BinaryCoordinateSweeps.Irrep.blockPerm line 111
  9. lemma OAI.BinaryCoordinateSweeps.Irrep.blockPerm_inr line 115
  10. lemma OAI.BinaryCoordinateSweeps.Irrep.blockPerm_of_fixed line 122
  11. def OAI.BinaryCoordinateSweeps.Irrep.basePlacement line 145
  12. lemma OAI.BinaryCoordinateSweeps.Irrep.placement_extension line 148
  13. def OAI.BinaryCoordinateSweeps.Irrep.placementSection line 151
  14. lemma OAI.BinaryCoordinateSweeps.Irrep.placementSection_apply line 154
  15. lemma OAI.BinaryCoordinateSweeps.Irrep.placementSection_covers line 158
  16. theorem OAI.BinaryCoordinateSweeps.Irrep.placement_coind_finrank line 172
  17. theorem OAI.BinaryCoordinateSweeps.Irrep.placement_coind_finrank_pow line 178