OAI/Analysis/FreeGroupFactor/TraceCocycle.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.TraceCocycle.CF line 15
  2. def OAI.FreeGroupFactorMain.TraceCocycle.shift line 17
  3. theorem OAI.FreeGroupFactorMain.TraceCocycle.shift_apply line 20
  4. theorem OAI.FreeGroupFactorMain.TraceCocycle.shift_one line 23
  5. theorem OAI.FreeGroupFactorMain.TraceCocycle.shift_mul line 27
  6. def OAI.FreeGroupFactorMain.TraceCocycle.action line 32
  7. def OAI.FreeGroupFactorMain.TraceCocycle.graph line 43
  8. theorem OAI.FreeGroupFactorMain.TraceCocycle.graph_right line 47
  9. def OAI.FreeGroupFactorMain.TraceCocycle.cocycle line 54
  10. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_of line 57
  11. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_one line 61
  12. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_mul line 64
  13. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_inv line 70
  14. def OAI.FreeGroupFactorMain.TraceCocycle.traceDerivative line 76
  15. theorem OAI.FreeGroupFactorMain.TraceCocycle.traceDerivative_conjugate line 79
  16. def OAI.FreeGroupFactorMain.TraceCocycle.CyclicConjugate line 87
  17. theorem OAI.FreeGroupFactorMain.TraceCocycle.CyclicConjugate.conj line 90
  18. theorem OAI.FreeGroupFactorMain.TraceCocycle.CyclicConjugate.inv line 95
  19. def OAI.FreeGroupFactorMain.TraceCocycle.SupportedOn line 100
  20. theorem OAI.FreeGroupFactorMain.TraceCocycle.supported_zero line 103
  21. theorem OAI.FreeGroupFactorMain.TraceCocycle.supported_add line 107
  22. theorem OAI.FreeGroupFactorMain.TraceCocycle.supported_neg line 112
  23. theorem OAI.FreeGroupFactorMain.TraceCocycle.supported_shift line 117
  24. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_supported line 132
  25. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_pow_zero line 141
  26. theorem OAI.FreeGroupFactorMain.TraceCocycle.cocycle_zpow_zero line 147
  27. theorem OAI.FreeGroupFactorMain.TraceCocycle.universalGroupTraceIdentity line 153
  28. def OAI.FreeGroupFactorMain.TraceCocycle.rightShift line 166
  29. theorem OAI.FreeGroupFactorMain.TraceCocycle.rightShift_apply line 169
  30. def OAI.FreeGroupFactorMain.TraceCocycle.polynomialDerivative line 172
  31. theorem OAI.FreeGroupFactorMain.TraceCocycle.polynomialDerivative_single line 176
  32. theorem OAI.FreeGroupFactorMain.TraceCocycle.polynomialDerivative_trace_zero line 181
  33. theorem OAI.FreeGroupFactorMain.TraceCocycle.iteratedDerivative_trace_zero line 193
  34. def OAI.FreeGroupFactorMain.TraceCocycle.algebraDerivative line 200
  35. theorem OAI.FreeGroupFactorMain.TraceCocycle.algebraDerivative_coeff line 205
  36. theorem OAI.FreeGroupFactorMain.TraceCocycle.algebraDerivative_of_coeff line 209
  37. theorem OAI.FreeGroupFactorMain.TraceCocycle.algebraDerivative_mul_of line 215
  38. theorem OAI.FreeGroupFactorMain.TraceCocycle.algebraDerivative_mul line 227
  39. def OAI.FreeGroupFactorMain.TraceCocycle.laurent line 239
  40. theorem OAI.FreeGroupFactorMain.TraceCocycle.supported_smul line 242
  41. theorem OAI.FreeGroupFactorMain.TraceCocycle.laurent_supported line 247
  42. def OAI.FreeGroupFactorMain.TraceCocycle.fieldCoefficients line 262
  43. theorem OAI.FreeGroupFactorMain.TraceCocycle.fieldCoefficients_supported line 268
  44. theorem OAI.FreeGroupFactorMain.TraceCocycle.sourceLaurentTraceIdentity line 281
  45. def OAI.FreeGroupFactorMain.AlgebraPolynomial.signed line 293
  46. def OAI.FreeGroupFactorMain.AlgebraPolynomial.wordExpr line 296
  47. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.eval_wordExpr line 300
  48. def OAI.FreeGroupFactorMain.AlgebraPolynomial.groupExpr line 311
  49. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.eval_groupExpr line 314
  50. def OAI.FreeGroupFactorMain.AlgebraPolynomial.sumExpr line 319
  51. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.eval_sumExpr line 323
  52. def OAI.FreeGroupFactorMain.AlgebraPolynomial.encode line 330
  53. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.eval_encode line 334
  54. def OAI.FreeGroupFactorMain.AlgebraPolynomial.encodedField line 345
  55. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.algebraDerivative_one line 349
  56. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.eval_delta_encoded line 355
  57. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.map_eval line 369
  58. theorem OAI.FreeGroupFactorMain.AlgebraPolynomial.encoded_initial_trace line 378