OAI/RepresentationTheory/FoulkesSixth/TensorPolarization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Foulkes.Polarization.P line 13
  2. def OAI.Foulkes.Polarization.weight line 15
  3. def OAI.Foulkes.Polarization.W line 17
  4. def OAI.Foulkes.Polarization.rowForm line 20
  5. def OAI.Foulkes.Polarization.pureRows line 23
  6. lemma OAI.Foulkes.Polarization.weight_apply_row line 26
  7. lemma OAI.Foulkes.Polarization.pureRows_mem line 35
  8. theorem OAI.Foulkes.Polarization.W_eq_span_pureRows line 53
  9. lemma OAI.Foulkes.Polarization.family_zero_of_all_shifted line 84
  10. def OAI.Foulkes.Polarization.z line 123
  11. def OAI.Foulkes.Polarization.polarizedSpan line 125
  12. lemma OAI.Foulkes.Polarization.eval_original_rowLinear line 129
  13. lemma OAI.Foulkes.Polarization.eval_family_empty line 136
  14. lemma OAI.Foulkes.Polarization.eval_family_univ line 143
  15. lemma OAI.Foulkes.Polarization.z_pow_mem line 152
  16. theorem OAI.Foulkes.Polarization.W_polarization line 158