OAI/NumberTheory/Ostmann/Characters/SourceTemplateDefs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceWidth line 13
  2. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceWidth_word line 19
  3. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceWidth_pivot line 21
  4. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceWidth_anchor line 25
  5. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceWidth_filler line 27
  6. abbrev OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.SourceConstituent line 30
  7. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.templateOriginalWord line 33
  8. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.templateWordMask line 37
  9. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.template_word_state line 41
  10. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.templateWordMask_eq_state_bin line 48