OAI/NumberTheory/Ostmann/Characters/TemplateResidueExposure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Characters.Template.KnownStates line 11
2. abbrev OAI.Ostmann.Characters.Template.PairedKnownStates line 12
3. theorem OAI.Ostmann.Characters.Template.frequency_dvd_precision line 14
4. def OAI.Ostmann.Characters.Template.ambientData line 17
5. def OAI.Ostmann.Characters.Template.knownCoefficient line 27
6. def OAI.Ostmann.Characters.Template.exposureConstraint line 32
7. def OAI.Ostmann.Characters.Template.exposureStep line 45
8. theorem OAI.Ostmann.Characters.Template.actual_residue_leaf_count line 60