OAI/NumberTheory/Jacobsthal/Siegel/LinearShearHom.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.totalDegree_aeval_le_of_linear line 16
  2. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.linearShearHom line 42
  3. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.linearShearHom_X_succ line 46
  4. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.linearShearHom_comp_neg line 50
  5. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.linearShear line 55
  6. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.totalDegree_linearShear_le line 60
  7. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.totalDegree_linearShear line 74
  8. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.isHomogeneous_linearShear line 84
  9. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eval_mul_of_isHomogeneous line 97
  10. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.exists_eval_cons_one_ne_zero line 114
  11. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.homogeneousComponent_linearShear line 136
  12. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eval_cons_one_zero_of_isHomogeneous line 148
  13. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eval_cons_one_zero_linearShear line 168
  14. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.algEquiv_isIntegral line 186
  15. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.isUnit_leadingCoeff_finSuccEquiv_of_full_degree line 190
  16. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationEquiv line 211
  17. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationIdeal line 215
  18. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationQuotientEquiv line 219
  19. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationBaseHom line 232
  20. def OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationHom line 238
  21. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationHom_isIntegral line 244
  22. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.linearShear_apply_neg line 268
  23. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationQuotientEquiv_mk line 274
  24. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationHom_apply_raw line 281
  25. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationEquiv_linearShear_neg line 287
  26. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationEquiv_symm_C_X line 292
  27. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationHom_X line 298
  28. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationHom_apply line 304
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_homogeneous_relation_not_dvd_coordinate line 323
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinate_dvd_sub_aeval_update_zero line 365
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.aeval_update_zero_eq_zero_iff line 382
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isHomogeneous_aeval_update_zero line 392
  33. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eval_aeval_update_zero line 409
  34. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.exists_eval_cons_one_with_zero line 425
  35. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.degreeOf_linearShear_eq_of_isHomogeneous line 442
  36. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.exists_linearShear_fix_coordinate_full line 457
  37. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.eliminationKer_isHomogeneous line 475
  38. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.homogeneous_prime_finOne_eq_bot line 493
  39. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.exists_integral_injective_linear_quotient_fixed_last line 527
  40. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.exists_integral_injective_linear_quotient_fixed_coordinate line 596
  41. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.finite_of_integral_quotient line 648
  42. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringKrullDim_eq_of_integral_faithful_goingDown line 665
  43. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ringKrullDim_eq_of_integral_faithful_normal line 680
  44. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.ringKrullDim_quotient_eq_normalization_variables line 693
  45. theorem OAI.Erdos970.WeightedTorusJets.LinearNormalization.exists_finite_linear_normalization_finite_variables line 717