OAI/GroupTheory/SimpleOvergroups/PolynomialNames.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.Name line 20
  2. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value line 22
  3. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_nil line 25
  4. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_cons line 26
  5. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_append line 28
  6. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.oneName line 31
  7. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_oneName line 32
  8. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.product line 35
  9. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_mul_term line 38
  10. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_product line 47
  11. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_surjective line 54
  12. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.cost line 69
  13. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.cost_le_iff line 73
  14. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.term_cost_le line 83
  15. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.mem_ball line 88
  16. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.collectName line 98
  17. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_collectName line 101
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.primrec_product line 119
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.primrec_cost line 129
  20. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.partialCollect line 136
  21. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.partialCollect_full line 141
  22. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.value_eq_iff_arrays line 151
  23. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.computable_value_eq line 163
  24. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.valueKey line 170
  25. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.valueKey_injective line 173
  26. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.valueKey_value line 177
  27. def OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.partialKey line 180
  28. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.partialKey_full line 184
  29. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.partrec_partialCollect line 192
  30. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Polynomial.partrec_partialKey line 208