OAI/NumberTheory/Ostmann/Construction/DiagonalCounterpartReindexBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.smallTransformGroupedBound line 16
2. def OAI.Ostmann.Construction.smallTransformCoefficientPairing line 24
3. def OAI.Ostmann.Construction.smallTransformCounterpartPairing line 34
4. theorem OAI.Ostmann.Construction.smallTransformGroupedBound_eq_coefficientPairing line 43
5. theorem OAI.Ostmann.Construction.smallTransformCoefficientPairing_eq_counterpartPairing line 72
6. theorem OAI.Ostmann.Construction.remainingDiagonal_le_small_counterpart_pairing line 91