OAI/NumberTheory/SiegelZeros/LocalAlgebra/LocalQuotientEquiv.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.isRegular_parameters_mvPolynomial_localization line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.localRingHom_surjective_of_surjective line 34
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.ker_localRingHom_of_surjective line 44
  4. def OAI.SiegelZeros.WeightedTorusJets.Deformation.localQuotientEquiv line 52
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.localQuotientEquiv_apply_mk_algebraMap line 61
  6. def OAI.SiegelZeros.WeightedTorusJets.Deformation.localQuotientAlgEquiv line 70
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.localQuotientAlgEquiv_apply_mk_algebraMap line 82
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.ker_mvPolynomial_evaluation line 92
  9. def OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialLocalQuotientAlgEquiv line 102
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.mvPolynomialLocalQuotientAlgEquiv_apply_mk_algebraMap line 127
  11. def OAI.SiegelZeros.WeightedTorusJets.Deformation.quotientFamilySpecializationAlgEquiv line 141
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.isRegular_quotient_iff line 164
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.isRegular_quotSMulTop_iff line 177
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.isRegular_mvPolynomial_localized_special_fiber line 191
  15. def OAI.SiegelZeros.WeightedTorusJets.polynomialDeformation line 228
  16. theorem OAI.SiegelZeros.WeightedTorusJets.polynomialDeformation_at_zero line 233
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.isRegular_source_polynomialDeformation_special_fiber line 244
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.parameter_regular_after_quotient line 271
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.flat_of_regular_uniformizer line 284
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.flat_quotient_of_regular_special_fiber line 295
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.dvr_polynomial_at_linear line 313
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.irreducible_parameter_at_linear line 321
  23. def OAI.SiegelZeros.WeightedTorusJets.Deformation.residueFieldAtLinearAlgEquiv line 334
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.specialFiber_prime_comap_C line 350
  25. def OAI.SiegelZeros.WeightedTorusJets.Deformation.parameterLocalAlgebra line 362
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.parameterLocalAlgebra_isScalarTower line 370
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.parameterLocalAlgebra_parameter line 384
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.parameterLocalAlgebra_groundFieldTower line 395
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.localized_polynomial_parameter_ne_zero line 405
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.parameterLocalAlgebra_parameter_regular line 417
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.flat_ideal_quotient_of_flat_smul_top line 434
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.ideal_ofList_ofFn_eq_span_range line 445
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.ideal_ofList_map_finRange_eq_span_range line 453
  34. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.flat_span_range_quotient_of_flat_ofFn_smul_top line 459
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.flat_polynomialDeformation_localized line 473