OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightPositiveSupportActual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivots_encode_node_iff line 11
2. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.pivotExpr_pos_of_encode_scalar_ne_zero line 27
3. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotCells_of_actualRealHistoryScalar_ne_zero line 39
4. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotsPositive_of_actualRealHistoryScalar_ne_zero line 45
5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualRealHistoryScalar_eq_zero_of_not_allPivotsPositive line 51
6. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotCells_of_actualRealXi_ne_zero line 58
7. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotsPositive_of_actualRealXi_ne_zero line 71
8. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualRealXi_eq_zero_of_not_allPivotsPositive line 81