OAI/NumberTheory/DirichletL/Dictionary/InverseMarkedPhysicalRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.actualRow line 18
2. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.actualRow_injective line 20
3. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.actual_rows_sum line 24
4. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.oriented_child line 28
5. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.physicalProduct_eq line 39
6. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.fiber_rows_le_deleted_sources line 47
7. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.fiber_child_rows_le_deleted_sources line 105
8. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPhysicalRows.actual_rows_norm line 129