OAI/NumberTheory/Jacobsthal/Siegel/DerivationJet.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mixed_iterate_add line 16
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mixed_derivation_pow_add line 29
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivation_pow_mixed_derivation_pow line 43
  4. lemma OAI.Erdos970.WeightedTorusJets.Geometry.extend_selectedIndex_eq_zero line 65
  5. lemma OAI.Erdos970.WeightedTorusJets.Geometry.extend_selectedIndex_le line 71
  6. lemma OAI.Erdos970.WeightedTorusJets.Geometry.extend_selectedIndex_single line 81
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.add_jet_indices_le_next_stage line 93
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.selectedIndex_add_stage_bound line 99
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.selectedIndex_add_stage_bound_lt line 104
  10. def OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet line 116
  11. def OAI.Erdos970.WeightedTorusJets.Geometry.derivativeStageIdeal line 119
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet_zero line 123
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_iff line 128
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet_map line 135
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivativeStageIdeal_map line 147
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationJet_shift line 155
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.single_index_le line 164
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.pair_index_le line 171
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.triple_index_le line 183
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_taylor_one line 199
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_taylor_two line 219
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivativeStageIdeal_le_ker_taylor_three line 246
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_module_length_eq_finrank line 289
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_length_eq_finrank line 303
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isNilpotent_of_mem_nilpotent_ideal line 309
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isLocalRing_of_nilpotent_augmentation line 317
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.residue_surjective_of_nilpotent_augmentation line 331
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.length_eq_finrank_of_nilpotent_augmentation line 345
  29. instance OAI.Erdos970.WeightedTorusJets.Geometry.finite_rectangularQuotient line 354
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ker_constantCoeff_eq_idealOfVars line 360
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isNilpotent_map_idealOfVars_of_pow_mem line 379
  32. def OAI.Erdos970.WeightedTorusJets.Geometry.quotientAugmentation line 392
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotientAugmentation_mk line 399
  34. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ker_quotientAugmentation line 406
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isNilpotent_ker_quotientAugmentation line 427
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularIdeal_le_ker_constantCoeff line 436
  37. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularAugmentation line 445
  38. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isNilpotent_ker_rectangularAugmentation line 451
  39. theorem OAI.Erdos970.WeightedTorusJets.Geometry.surjective_of_nilpotent_ideal_lifts line 466