OAI/NumberTheory/SiegelZeros/Intersection/LocalIntersectionFormula.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.finite_length_kernel_eq_cokernel line 23
2. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMul line 44
3. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMul_apply line 47
4. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMul_mk line 50
5. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMul_kernel line 57
6. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.colonQuotientEquivKernel line 76
7. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMul_range line 82
8. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cokernelEquivCut line 94
9. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.kernel_length_eq_colon line 100
10. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cokernel_length_eq_cut line 105
11. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.finite_length_cut_eq_colon line 110
12. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.regular_colon_length_zero line 117
13. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.prime_quotientMul_injective line 131
14. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.prime_colon_length_zero line 140
15. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMul_eq_zero_of_mem line 145
16. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.minimalPrimeCutSum line 154
17. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.LocalOneCutLengthStatement line 166
18. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.map_scalar_kernel line 184
19. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.map_scalar_range line 199
20. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.scalarKernelEquiv line 213
21. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.scalarCokernelEquiv line 218
22. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.scalar_kernel_length_eq line 223
23. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.scalar_cokernel_length_eq line 228
24. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cyclic_factor_kernel_length line 233
25. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cyclic_factor_cokernel_length line 242
26. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotient_annihilator_eq_colon line 263
27. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.exists_cyclic_prime_filtration_nat line 271
28. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.exists_cyclic_filtration_all_local_counts line 318
29. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.maximal_factor_cut_eq_colon line 343
30. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.regular_not_mem_minimalPrime line 353
31. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.dimension_one_prime_factor_dichotomy line 358
32. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.scalar_euler_cross_add line 382
33. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cyclic_ideal_step_cross_add line 401
34. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cutEuler line 439
35. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.finite_cross_add_to_integer line 443
36. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cutEuler_cyclic_step line 459
37. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cutEuler_top line 469
38. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cutEuler_filtration line 472
39. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.exists_prime_factor_euler_sum line 486
40. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.regular_cut_length_ne_top line 510
41. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.regular_colon_length_ne_top line 516
42. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.regular_colon_bot line 523
43. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cutEuler_bot_regular line 530
44. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.cutEuler_prime_regular line 544
45. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.exists_regular_onecut_sum_and_local_counts line 556
46. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.subtype_indicator_sum line 592
47. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.regular_ring_onecut_length line 617
48. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotient_cut_length line 681
49. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotient_principal_cut_length line 695
50. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotient_prime_cut_length line 704
51. def OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMinimalPrimesEquiv line 724
52. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotientMinimalPrimesEquiv_apply line 743
53. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotient_minimal_local_length line 747
54. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.minimalPrimeCutSum_quotient line 786
55. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.quotient_parameter_mem_nonZeroDivisors line 809
56. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.local_onecut_length line 819
57. theorem OAI.SiegelZeros.WeightedTorusJets.W28.LocalIntersection.localOneCutLengthStatement_proved line 841