OAI/NumberTheory/SiegelZeros/LocalAlgebra/NormalizationPresentationLocalEquiv.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentationLocalEquiv line 24
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentationLocalEquiv_algebraMap line 32
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.totalDegree_eval₂_le_of_linear_images line 52
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_finrank_le_pow line 84
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.totalDegree_normalizationPresentation_le line 120
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.totalDegree_localized_normalizationPresentation_le line 139
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalizationPresentation_radical_eq_maximal line 148
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finrank_eq_length_mul_residue_degree line 173
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finrank_localization_le line 186
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.component_local_artinian line 202
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.component_local_length_ne_top line 209
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_component_regular line 222
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.regular_localization_component line 225
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.regular_localization_component_cotangent_dim line 231
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_component_height_bounds line 241
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_component_cotangent_dim line 253
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localization_component_cotangent_bounds line 260
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.map_extended_ideal_eq line 282
  19. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.quotientExtendedAlgEquiv line 289
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.extended_quotient_length_eq line 295
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.local_quotient_length_eq_after_localization line 302
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.field_length_eq_local_length_mul_residue_length line 322
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.finite_of_finite_length_of_finite_residue line 328
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.finrank_eq_local_length_toNat_mul_residue_degree line 341
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.local_weighted_length_le_finrank line 351
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.finrank_eq_sum_local_length_mul_residue_degree line 365
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.finite_residue_of_maximal line 389
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.isolated_quotient_finite line 399
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.isolated_component_finrank line 407
  30. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficientLocalizationResidueAlgEquiv line 425
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_residue_degree_eq_rank line 438
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.projected_residue_degree_eq_component_rank line 451
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_quotient_length line 464
  34. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_component_finrank line 481
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_component_finrank_eq_length_mul_rank line 509