OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedSpectatorSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySignedSpectator.GiantOutsideUnits line 12
2. def OAI.Ostmann.Arithmetic.HistorySignedSpectator.OutsideUnits line 15
3. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.OutsideUnits.root line 21
4. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.spectatorFactor_component_ne_zero line 27
5. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.spectatorFactor_denominator_ne_zero line 35
6. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.spectatorFactor_nonzero_giantOutsideUnits line 43
7. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.spectatorProduct_nonzero_rebuild_outsideUnits line 63
8. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.pairSpectator_nonzero_rebuild_outsideUnits line 96
9. theorem OAI.Ostmann.Arithmetic.HistorySignedSpectator.pairSpectator_eq_zero_of_not_rebuild_outsideUnits line 111