OAI/NumberTheory/DirichletL/Inversion/InitialMarkedAssignedGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assignedGenerator line 15
2. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assignedGenerator_mem line 19
3. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assignedGenerator_span line 24
4. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assignedGenerator_ne_zero line 29
5. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assignedElement_span line 35
6. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assignedGenerator_window_live line 44
7. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assigned_ratio_product line 53
8. theorem OAI.SevenEighths.InverseInitialMarkedAssignedGeometry.assigned_ratio_interval line 61