OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedDecodeXi.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySignedDecode.signedGiantSample line 12
2. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.symbolicHistory_rebuild_giantsAgree line 18
3. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.symbolicHistory_allPivotsPositive_iff_rebuild line 29
4. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.actualScalar_ne_zero_rebuild_pivotsPositive line 38
5. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.actualXi_ne_zero_rebuild_positiveIntegral line 47
6. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.actualXi_eq_zero_of_not_rebuild_pivotsPositive line 64