OAI/NumberTheory/Jacobsthal/Siegel/NormalizationPresentationLocalEquiv.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentationLocalEquiv line 30
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentationLocalEquiv_algebraMap line 38
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.totalDegree_eval₂_le_of_linear_images line 58
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_finrank_le_pow line 90
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.totalDegree_normalizationPresentation_le line 126
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.totalDegree_localized_normalizationPresentation_le line 145
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_radical_eq_maximal line 154
  8. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finrank_eq_length_mul_residue_degree line 179
  9. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finrank_localization_le line 192
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.component_local_artinian line 208
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.component_local_length_ne_top line 215
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_component_regular line 228
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.regular_localization_component line 231
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.regular_localization_component_cotangent_dim line 237
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_component_height_bounds line 247
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_component_cotangent_dim line 259
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localization_component_cotangent_bounds line 266
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.map_extended_ideal_eq line 288
  19. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.quotientExtendedAlgEquiv line 295
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.extended_quotient_length_eq line 301
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.local_quotient_length_eq_after_localization line 308
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.field_length_eq_local_length_mul_residue_length line 328
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.finite_of_finite_length_of_finite_residue line 334
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.finrank_eq_local_length_toNat_mul_residue_degree line 347
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.local_weighted_length_le_finrank line 358
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.finrank_eq_sum_local_length_mul_residue_degree line 372
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.finite_residue_of_maximal line 397
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.isolated_quotient_finite line 407
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.isolated_component_finrank line 415
  30. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficientLocalizationResidueAlgEquiv line 433
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_residue_degree_eq_rank line 446
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.projected_residue_degree_eq_component_rank line 459
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_quotient_length line 472
  34. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_component_finrank line 489
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_component_finrank_eq_length_mul_rank line 517