OAI/NumberTheory/Ostmann/QuadraticCenter/KernelPopulation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.kernelRootResidues line 8
2. theorem OAI.Ostmann.QuadraticCenter.mem_kernelRootResidues line 13
3. theorem OAI.Ostmann.QuadraticCenter.squareFactor_mod_mem_kernelRootResidues line 19
4. theorem OAI.Ostmann.QuadraticCenter.kernel_population_le_quotient_interval line 27
5. theorem OAI.Ostmann.QuadraticCenter.kernel_population_le_diameter line 59
6. theorem OAI.Ostmann.QuadraticCenter.nonnegative_square_diameter line 79
7. theorem OAI.Ostmann.QuadraticCenter.kernel_squareFactor_diameter line 91