OAI/NumberTheory/SiegelZeros/Differentials/DerivationJet.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mixed_iterate_add line 13
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mixed_derivation_pow_add line 26
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivation_pow_mixed_derivation_pow line 40
  4. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.extend_selectedIndex_eq_zero line 62
  5. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.extend_selectedIndex_le line 68
  6. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.extend_selectedIndex_single line 78
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.add_jet_indices_le_next_stage line 90
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.selectedIndex_add_stage_bound line 96
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.selectedIndex_add_stage_bound_lt line 101
  10. def OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet line 113
  11. def OAI.SiegelZeros.WeightedTorusJets.Geometry.derivativeStageIdeal line 116
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet_zero line 120
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_iff line 125
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet_map line 132
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivativeStageIdeal_map line 144
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationJet_shift line 152
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.single_index_le line 161
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.pair_index_le line 168
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.triple_index_le line 180
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_taylor_one line 196
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_taylor_two line 216
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_taylor_three line 243
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_module_length_eq_finrank line 286
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_length_eq_finrank line 300
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isNilpotent_of_mem_nilpotent_ideal line 306
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isLocalRing_of_nilpotent_augmentation line 314
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.residue_surjective_of_nilpotent_augmentation line 328
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.length_eq_finrank_of_nilpotent_augmentation line 342
  29. instance OAI.SiegelZeros.WeightedTorusJets.Geometry.finite_rectangularQuotient line 351
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ker_constantCoeff_eq_idealOfVars line 357
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isNilpotent_map_idealOfVars_of_pow_mem line 376
  32. def OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientAugmentation line 389
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientAugmentation_mk line 396
  34. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ker_quotientAugmentation line 403
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isNilpotent_ker_quotientAugmentation line 424
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularIdeal_le_ker_constantCoeff line 433
  37. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularAugmentation line 442
  38. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isNilpotent_ker_rectangularAugmentation line 448
  39. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.surjective_of_nilpotent_ideal_lifts line 460