OAI/NumberTheory/Ostmann/Construction/Diagonal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.groupedValue line 12
2. def OAI.Ostmann.Construction.diagonalComplex line 15
3. def OAI.Ostmann.Construction.offDiagonalComplex line 18
4. theorem OAI.Ostmann.Construction.diagonal_add_offDiagonal line 21
5. theorem OAI.Ostmann.Construction.diagonal_eq_grouped_squares line 33
6. theorem OAI.Ostmann.Construction.diagonal_nonneg line 62
7. theorem OAI.Ostmann.Construction.diagonal_real line 68
8. theorem OAI.Ostmann.Construction.offDiagonal_real line 73
9. theorem OAI.Ostmann.Construction.square_split line 79
10. theorem OAI.Ostmann.Construction.ratio_tag_eq_iff line 88