OAI/NumberTheory/Jacobsthal/Siegel/LocalFractionAlgebra.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.generic_homogeneous_deformation_quotient_bound line 23
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_lift_of_mem_leadingFormIdeal line 48
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneousComponent_mem_leadingFormIdeal line 84
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.eq_zero_or_totalDegree_lt_of_homogeneousComponent_eq_zero line 94
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.representatives_of_homogeneous_lifts line 114
  6. theorem OAI.Erdos970.WeightedTorusJets.exists_monomial_basis_quotient line 162
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneousComponent_mem_span_monomials line 199
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_span_eq_top_iff_representatives line 215
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finite_and_finrank_le_leadingFormQuotient line 238
  10. theorem OAI.Erdos970.WeightedTorusJets.polynomialDeformation_totalDegree_le line 269
  11. theorem OAI.Erdos970.WeightedTorusJets.map_polynomialDeformation_totalDegree_le line 282
  12. theorem OAI.Erdos970.WeightedTorusJets.generic_affine_deformation_quotient_bound line 295
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.maximal_polynomial_height line 337
  14. def OAI.Erdos970.WeightedTorusJets.Deformation.localFractionAlgebra line 365
  15. theorem OAI.Erdos970.WeightedTorusJets.Deformation.localFractionAlgebra_isScalarTower line 375
  16. theorem OAI.Erdos970.WeightedTorusJets.Deformation.localFractionAlgebra_isFractionRing line 386
  17. theorem OAI.Erdos970.WeightedTorusJets.Deformation.surjective_baseChange_localization line 406
  18. theorem OAI.Erdos970.WeightedTorusJets.Deformation.surjective_baseChange_localized_quotient line 428
  19. def OAI.Erdos970.WeightedTorusJets.Deformation.genericFiberLocalBaseEquiv line 446
  20. def OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialQuotientBaseChange line 463
  21. theorem OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialQuotientBaseChange_tmul_mk line 479
  22. def OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialSpanQuotientBaseChange line 488
  23. theorem OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialSpanQuotientBaseChange_tmul_mk line 496
  24. theorem OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialSpanQuotientBaseChange_symm_mk_map line 504