OAI/NumberTheory/Ostmann/Construction/RemainingDiagonal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Construction.RemainingTerm line 18
2. def OAI.Ostmann.Construction.remainingTermMass line 21
3. def OAI.Ostmann.Construction.remainingTermExactTag line 24
4. def OAI.Ostmann.Construction.remainingTermModularTag line 27
5. def OAI.Ostmann.Construction.remainingTermValue line 32
6. def OAI.Ostmann.Construction.remainingDiagonal line 35
7. def OAI.Ostmann.Construction.remainingOffDiagonal line 40
8. theorem OAI.Ostmann.Construction.remainingDiagonal_nonneg line 46
9. theorem OAI.Ostmann.Construction.remainingRowSquare_split line 50