`OAI/NumberTheory/Ostmann/Characters/QuartetProjectedCut.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional projected norm bound on the actual tree cut

theorem OAI.Ostmann.projectedTree_valid_cut_le line 18