OAI/NumberTheory/Ostmann/Characters/FrequencyTreeSum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.FrequencyTreeSum.Assignment line 11
  2. instance OAI.Ostmann.Characters.FrequencyTreeSum.assignmentFintype line 16
  3. def OAI.Ostmann.Characters.FrequencyTreeSum.root line 25
  4. theorem OAI.Ostmann.Characters.FrequencyTreeSum.root_mem line 29
  5. def OAI.Ostmann.Characters.FrequencyTreeSum.weight line 35
  6. def OAI.Ostmann.Characters.FrequencyTreeSum.total line 41
  7. def OAI.Ostmann.Characters.FrequencyTreeSum.budget line 44
  8. theorem OAI.Ostmann.Characters.FrequencyTreeSum.weight_nonneg line 48
  9. theorem OAI.Ostmann.Characters.FrequencyTreeSum.budget_nonneg line 55
  10. theorem OAI.Ostmann.Characters.FrequencyTreeSum.total_succ line 61
  11. theorem OAI.Ostmann.Characters.FrequencyTreeSum.total_le_budget line 81