OAI/NumberTheory/Ostmann/Characters/TemplateSymbolic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.Template.finiteProductExpression line 13
  2. theorem OAI.Ostmann.Characters.Template.finiteProductExpression_eval line 17
  3. theorem OAI.Ostmann.Characters.Template.finiteProductExpression_good line 22
  4. abbrev OAI.Ostmann.Characters.Template.Expressions line 31
  5. def OAI.Ostmann.Characters.Template.evalExpressions line 33
  6. def OAI.Ostmann.Characters.Template.copiedExpression line 36
  7. def OAI.Ostmann.Characters.Template.pivotExpression line 40
  8. def OAI.Ostmann.Characters.Template.childExpressions line 44
  9. theorem OAI.Ostmann.Characters.Template.copiedExpression_eval line 50
  10. theorem OAI.Ostmann.Characters.Template.pivotExpression_eval line 54
  11. theorem OAI.Ostmann.Characters.Template.childExpressions_eval line 59
  12. theorem OAI.Ostmann.Characters.Template.childExpressions_preserves line 67
  13. theorem OAI.Ostmann.Characters.Template.pivotExpression_good line 77
  14. def OAI.Ostmann.Characters.Template.pivots line 91
  15. def OAI.Ostmann.Characters.Template.pivotExpressions line 98
  16. theorem OAI.Ostmann.Characters.Template.pivotExpressions_eval line 106
  17. theorem OAI.Ostmann.Characters.Template.pivotExpressions_good line 114
  18. theorem OAI.Ostmann.Characters.Template.pivot_cleared line 143