OAI/NumberTheory/Ostmann/Construction/FiniteMatchedSupportedWindow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Counterpart normalization on the live coefficient support

  1. theorem OAI.Ostmann.finite_matched_supported_window_eq line 9
  2. theorem OAI.Ostmann.finite_matched_supported_window_bound line 41