OAI/NumberTheory/Ostmann/Arithmetic/HistoryFieldIndependence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryFieldIndependence.determinant line 13
2. def OAI.Ostmann.Arithmetic.HistoryFieldIndependence.Independent line 16
3. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.product_nonzero line 19
4. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.product_ofFn_nonzero line 26
5. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.append_nonzero line 34
6. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.determinant_left line 50
7. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.determinant_right line 63
8. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.child_independent line 76
9. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.nodeNumerator_nonzero line 101
10. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.encode_occurrence_nonzero line 119
11. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.canonical_nonzero line 161
12. theorem OAI.Ostmann.Arithmetic.HistoryFieldIndependence.canonical_regular line 178