OAI/NumberTheory/Ostmann/Characters/TemplateLeafSymbolic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.Template.BottomExpression line 11
  2. def OAI.Ostmann.Characters.Template.bottomExpressions line 13
  3. def OAI.Ostmann.Characters.Template.evalBottom line 21
  4. theorem OAI.Ostmann.Characters.Template.bottomExpressions_eval line 24
  5. theorem OAI.Ostmann.Characters.Template.bottomExpressions_length line 33
  6. def OAI.Ostmann.Characters.Template.periodExpression line 39
  7. theorem OAI.Ostmann.Characters.Template.periodExpression_eval line 41
  8. theorem OAI.Ostmann.Characters.Template.bottomExpressions_good line 45
  9. theorem OAI.Ostmann.Characters.Template.bottom_period_cleared line 72
  10. theorem OAI.Ostmann.Characters.Template.weight_eq_symbolic_profiles line 85