OAI/NumberTheory/Ostmann/Characters/TemplateCompositePivotSupportOrigins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Characters.Template.SampleOrigins line 11
  2. def OAI.Ostmann.Characters.Template.SampleOrigins.root line 18
  3. def OAI.Ostmann.Characters.Template.SampleOrigins.child line 22
  4. theorem OAI.Ostmann.Characters.Template.SampleOrigins.outside_exists line 38
  5. def OAI.Ostmann.Characters.Template.SampleOrigins.outside line 48
  6. theorem OAI.Ostmann.Characters.Template.SampleOrigins.origin_outside line 52
  7. def OAI.Ostmann.Characters.Template.SampleOrigins.Matches line 56
  8. theorem OAI.Ostmann.Characters.Template.SampleOrigins.root_matches line 59
  9. theorem OAI.Ostmann.Characters.Template.SampleOrigins.Matches.child line 64
  10. theorem OAI.Ostmann.Characters.Template.SampleOrigins.Matches.outside line 78