OAI/NumberTheory/Ostmann/QuadraticCenter/KernelFactorization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.QuadraticCenter.KernelFactorization line 7
2. theorem OAI.Ostmann.QuadraticCenter.exists_kernelFactorization line 14
3. def OAI.Ostmann.QuadraticCenter.kernelFactorization line 24
4. theorem OAI.Ostmann.QuadraticCenter.KernelFactorization.kernel_ne_zero line 30
5. theorem OAI.Ostmann.QuadraticCenter.KernelFactorization.kernel_dvd line 32
6. theorem OAI.Ostmann.QuadraticCenter.KernelFactorization.abs_factorization line 34
7. theorem OAI.Ostmann.QuadraticCenter.KernelFactorization.kernel_abs_le line 38
8. theorem OAI.Ostmann.QuadraticCenter.KernelFactorization.kernel_isCoprime line 42
9. theorem OAI.Ostmann.QuadraticCenter.KernelFactorization.squareFactor_isCoprime line 47