OAI/NumberTheory/Ostmann/Construction/ActualRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.residueTransform_sq_sum line 12
2. theorem OAI.Ostmann.Construction.giantResidueTransform_sq_sum_le line 21
3. def OAI.Ostmann.Construction.extractedUnits line 31
4. def OAI.Ostmann.Construction.actualExtractedRow line 37
5. theorem OAI.Ostmann.Construction.actualExtractedRow_apply line 44
6. theorem OAI.Ostmann.Construction.actualExtractedRow_sq_norm_le line 54
7. theorem OAI.Ostmann.Construction.actual_extracted_row_transfer line 65