OAI/NumberTheory/Jacobsthal/Siegel/PolynomialLinearCoefficients.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mem_vars_square_iff line 19
  2. def OAI.Erdos970.WeightedTorusJets.Geometry.polynomialLinearCoefficients line 33
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomialLinearCoefficients_apply line 37
  4. def OAI.Erdos970.WeightedTorusJets.Geometry.varsCotangentCoefficients line 41
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.varsCotangentCoefficients_toCotangent line 50
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.varsCotangentCoefficients_injective line 55
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.varsCotangentCoefficients_surjective line 66
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.varsCotangentEquiv line 81
  9. def OAI.Erdos970.WeightedTorusJets.Geometry.quotientVarsCotangentMap line 86
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotientVarsCotangentMap_surjective line 93
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotientVarsCotangentMap_injective line 106
  12. def OAI.Erdos970.WeightedTorusJets.Geometry.polynomialQuotientCotangentEquiv line 122
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomialQuotientCotangentEquiv_map_toCotangent line 129
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularIdeal_le_vars_square line 142
  15. def OAI.Erdos970.WeightedTorusJets.Geometry.cotangentEquivOfEqOver line 156
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.cotangentEquivOfEqOver_toCotangent line 162
  17. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularAugmentationCotangentEquiv line 169
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularAugmentationCotangentEquiv_toCotangent_mk line 177
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularAugmentation_linear_representative line 206
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.taylor_sum_sub_first_order_mem line 251
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringHom_comp_sub_first_order_mem line 267
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.truncatedTaylor_sub_first_order_mem line 280
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.truncatedTaylor_sub_self_mem line 287
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.truncatedTaylor_sub_self_mem_sq line 296
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringHom_comp3_sub_first_order_mem line 309
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_mem_vars line 329
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorAlong_sub_first_order_mem line 344
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorAlong_sub_self_mem line 354
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorAlong_sub_self_mem_sq line 362
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorComp3_sub_first_order_mem line 372
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularMap_vars_le line 399
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_sub_first_order_mem line 411
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_X_mul_C line 441
  34. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangular_augmentation_ker_eq line 448
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_one_first_order line 454
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_two_first_order line 476
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_three_first_order line 494