OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedTerminalIntegerPriorBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIndex line 21
  2. def OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerSupport line 24
  3. def OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerWeight line 27
  4. def OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceNaturalSupport line 30
  5. theorem OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerWeight_cast line 33
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourcePrior_cmean_integer line 38
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourcePrior_cmean_eq_integer line 44
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSource_support_exists_prime line 51
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminal_sourceHistoryPairMean_eq_integer line 62