OAI/NumberTheory/SiegelZeros/Structure/LinearShearHom.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.totalDegree_aeval_le_of_linear line 13
  2. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.linearShearHom line 39
  3. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.linearShearHom_X_succ line 43
  4. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.linearShearHom_comp_neg line 47
  5. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.linearShear line 52
  6. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.totalDegree_linearShear_le line 57
  7. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.totalDegree_linearShear line 71
  8. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.isHomogeneous_linearShear line 81
  9. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eval_mul_of_isHomogeneous line 94
  10. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.exists_eval_cons_one_ne_zero line 111
  11. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.homogeneousComponent_linearShear line 133
  12. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eval_cons_one_zero_of_isHomogeneous line 145
  13. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eval_cons_one_zero_linearShear line 165
  14. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.algEquiv_isIntegral line 183
  15. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.isUnit_leadingCoeff_finSuccEquiv_of_full_degree line 187
  16. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationEquiv line 208
  17. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationIdeal line 212
  18. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationQuotientEquiv line 216
  19. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationBaseHom line 229
  20. def OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationHom line 235
  21. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationHom_isIntegral line 241
  22. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.linearShear_apply_neg line 265
  23. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationQuotientEquiv_mk line 271
  24. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationHom_apply_raw line 278
  25. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationEquiv_linearShear_neg line 284
  26. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationEquiv_symm_C_X line 289
  27. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationHom_X line 295
  28. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationHom_apply line 301
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_homogeneous_relation_not_dvd_coordinate line 320
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinate_dvd_sub_aeval_update_zero line 362
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.aeval_update_zero_eq_zero_iff line 379
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isHomogeneous_aeval_update_zero line 389
  33. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eval_aeval_update_zero line 406
  34. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.exists_eval_cons_one_with_zero line 422
  35. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.degreeOf_linearShear_eq_of_isHomogeneous line 439
  36. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.exists_linearShear_fix_coordinate_full line 454
  37. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.eliminationKer_isHomogeneous line 472
  38. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.homogeneous_prime_finOne_eq_bot line 490
  39. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.exists_integral_injective_linear_quotient_fixed_last line 524
  40. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.exists_integral_injective_linear_quotient_fixed_coordinate line 593
  41. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.finite_of_integral_quotient line 645
  42. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringKrullDim_eq_of_integral_faithful_goingDown line 662
  43. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ringKrullDim_eq_of_integral_faithful_normal line 677
  44. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.ringKrullDim_quotient_eq_normalization_variables line 690
  45. theorem OAI.SiegelZeros.WeightedTorusJets.LinearNormalization.exists_finite_linear_normalization_finite_variables line 714