OAI/Combinatorics/Chromatic/QuantumTorus/GlobalFiberBound.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ElementaryPositivity.QuantumTorus.simple_fiber_bound_throughline 19 - theorem
OAI.ElementaryPositivity.QuantumTorus.simple_fiber_boundline 49 - theorem
OAI.ElementaryPositivity.QuantumTorus.simple_fiber_log_boundline 61