OAI/NumberTheory/Ostmann/Construction/DyadicGuardedGraph.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Whole-range one-sided cancellation for the supported quotient graph

  1. theorem OAI.Ostmann.dyadic_guarded_graph_bound line 12