OAI/NumberTheory/Ostmann/Quadratic/QuadraticTransformedComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two literal transformed main terms have the required cutoff saving

  1. theorem OAI.Ostmann.quadratic_transformed_main_comparison line 13