OAI/NumberTheory/Ostmann/Arithmetic/HistorySymbolicRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistorySymbolicRows.Row line 10
2. def OAI.Ostmann.Arithmetic.HistorySymbolicRows.evalRow line 12
3. def OAI.Ostmann.Arithmetic.HistorySymbolicRows.pivotRow line 15
4. theorem OAI.Ostmann.Arithmetic.HistorySymbolicRows.eval_pivotRow line 18
5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicRows.pivot_eval_eq_row line 27
6. def OAI.Ostmann.Arithmetic.HistorySymbolicRows.determinant line 35
7. theorem OAI.Ostmann.Arithmetic.HistorySymbolicRows.determinant_plus_pivot line 38
8. theorem OAI.Ostmann.Arithmetic.HistorySymbolicRows.determinant_pivot_minus line 46
9. theorem OAI.Ostmann.Arithmetic.HistorySymbolicRows.determinant_plus_pivot_ne_zero line 54
10. theorem OAI.Ostmann.Arithmetic.HistorySymbolicRows.determinant_pivot_minus_ne_zero line 63