OAI/NumberTheory/SiegelZeros/LocalAlgebra/PolynomialLinearCoefficients.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mem_vars_square_iff line 15
  2. def OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialLinearCoefficients line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialLinearCoefficients_apply line 33
  4. def OAI.SiegelZeros.WeightedTorusJets.Geometry.varsCotangentCoefficients line 37
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.varsCotangentCoefficients_toCotangent line 46
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.varsCotangentCoefficients_injective line 51
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.varsCotangentCoefficients_surjective line 62
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.varsCotangentEquiv line 77
  9. def OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientVarsCotangentMap line 82
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientVarsCotangentMap_surjective line 89
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientVarsCotangentMap_injective line 102
  12. def OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialQuotientCotangentEquiv line 118
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialQuotientCotangentEquiv_map_toCotangent line 125
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularIdeal_le_vars_square line 138
  15. def OAI.SiegelZeros.WeightedTorusJets.Geometry.cotangentEquivOfEqOver line 152
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.cotangentEquivOfEqOver_toCotangent line 158
  17. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularAugmentationCotangentEquiv line 165
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularAugmentationCotangentEquiv_toCotangent_mk line 173
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularAugmentation_linear_representative line 202
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.taylor_sum_sub_first_order_mem line 246
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringHom_comp_sub_first_order_mem line 262
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.truncatedTaylor_sub_first_order_mem line 275
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.truncatedTaylor_sub_self_mem line 282
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.truncatedTaylor_sub_self_mem_sq line 291
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringHom_comp3_sub_first_order_mem line 304
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_mem_vars line 324
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorAlong_sub_first_order_mem line 339
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorAlong_sub_self_mem line 349
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorAlong_sub_self_mem_sq line 357
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorComp3_sub_first_order_mem line 367
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularMap_vars_le line 394
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_sub_first_order_mem line 406
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_X_mul_C line 436
  34. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangular_augmentation_ker_eq line 443
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_one_first_order line 449
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_two_first_order line 471
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_three_first_order line 489