OAI/NumberTheory/SiegelZeros/LocalAlgebra/LocalFractionAlgebra.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.generic_homogeneous_deformation_quotient_bound line 20
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_lift_of_mem_leadingFormIdeal line 45
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneousComponent_mem_leadingFormIdeal line 81
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.eq_zero_or_totalDegree_lt_of_homogeneousComponent_eq_zero line 91
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.representatives_of_homogeneous_lifts line 111
  6. theorem OAI.SiegelZeros.WeightedTorusJets.exists_monomial_basis_quotient line 159
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneousComponent_mem_span_monomials line 196
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_span_eq_top_iff_representatives line 212
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finite_and_finrank_le_leadingFormQuotient line 235
  10. theorem OAI.SiegelZeros.WeightedTorusJets.polynomialDeformation_totalDegree_le line 266
  11. theorem OAI.SiegelZeros.WeightedTorusJets.map_polynomialDeformation_totalDegree_le line 279
  12. theorem OAI.SiegelZeros.WeightedTorusJets.generic_affine_deformation_quotient_bound line 292
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.maximal_polynomial_height line 333
  14. def OAI.SiegelZeros.WeightedTorusJets.Deformation.localFractionAlgebra line 359
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.localFractionAlgebra_isScalarTower line 369
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.localFractionAlgebra_isFractionRing line 380
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.surjective_baseChange_localization line 398
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.surjective_baseChange_localized_quotient line 420
  19. def OAI.SiegelZeros.WeightedTorusJets.Deformation.genericFiberLocalBaseEquiv line 438
  20. def OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialQuotientBaseChange line 455
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialQuotientBaseChange_tmul_mk line 471
  22. def OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialSpanQuotientBaseChange line 480
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialSpanQuotientBaseChange_tmul_mk line 488
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialSpanQuotientBaseChange_symm_mk_map line 496