OAI/NumberTheory/Jacobsthal/Siegel/LocalQuotientEquiv.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.isRegular_parameters_mvPolynomial_localization line 22
  2. theorem OAI.Erdos970.WeightedTorusJets.Deformation.localRingHom_surjective_of_surjective line 37
  3. theorem OAI.Erdos970.WeightedTorusJets.Deformation.ker_localRingHom_of_surjective line 47
  4. def OAI.Erdos970.WeightedTorusJets.Deformation.localQuotientEquiv line 55
  5. theorem OAI.Erdos970.WeightedTorusJets.Deformation.localQuotientEquiv_apply_mk_algebraMap line 64
  6. def OAI.Erdos970.WeightedTorusJets.Deformation.localQuotientAlgEquiv line 73
  7. theorem OAI.Erdos970.WeightedTorusJets.Deformation.localQuotientAlgEquiv_apply_mk_algebraMap line 85
  8. theorem OAI.Erdos970.WeightedTorusJets.Deformation.ker_mvPolynomial_evaluation line 95
  9. def OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialLocalQuotientAlgEquiv line 105
  10. theorem OAI.Erdos970.WeightedTorusJets.Deformation.mvPolynomialLocalQuotientAlgEquiv_apply_mk_algebraMap line 130
  11. def OAI.Erdos970.WeightedTorusJets.Deformation.quotientFamilySpecializationAlgEquiv line 144
  12. theorem OAI.Erdos970.WeightedTorusJets.Deformation.isRegular_quotient_iff line 167
  13. theorem OAI.Erdos970.WeightedTorusJets.Deformation.isRegular_quotSMulTop_iff line 180
  14. theorem OAI.Erdos970.WeightedTorusJets.Deformation.isRegular_mvPolynomial_localized_special_fiber line 194
  15. def OAI.Erdos970.WeightedTorusJets.polynomialDeformation line 231
  16. theorem OAI.Erdos970.WeightedTorusJets.polynomialDeformation_at_zero line 236
  17. theorem OAI.Erdos970.WeightedTorusJets.Deformation.isRegular_source_polynomialDeformation_special_fiber line 247
  18. theorem OAI.Erdos970.WeightedTorusJets.Deformation.parameter_regular_after_quotient line 274
  19. theorem OAI.Erdos970.WeightedTorusJets.Deformation.flat_of_regular_uniformizer line 287
  20. theorem OAI.Erdos970.WeightedTorusJets.Deformation.flat_quotient_of_regular_special_fiber line 298
  21. theorem OAI.Erdos970.WeightedTorusJets.Deformation.dvr_polynomial_at_linear line 316
  22. theorem OAI.Erdos970.WeightedTorusJets.Deformation.irreducible_parameter_at_linear line 324
  23. def OAI.Erdos970.WeightedTorusJets.Deformation.residueFieldAtLinearAlgEquiv line 337
  24. theorem OAI.Erdos970.WeightedTorusJets.Deformation.specialFiber_prime_comap_C line 353
  25. def OAI.Erdos970.WeightedTorusJets.Deformation.parameterLocalAlgebra line 365
  26. theorem OAI.Erdos970.WeightedTorusJets.Deformation.parameterLocalAlgebra_isScalarTower line 373
  27. theorem OAI.Erdos970.WeightedTorusJets.Deformation.parameterLocalAlgebra_parameter line 387
  28. theorem OAI.Erdos970.WeightedTorusJets.Deformation.parameterLocalAlgebra_groundFieldTower line 398
  29. theorem OAI.Erdos970.WeightedTorusJets.Deformation.localized_polynomial_parameter_ne_zero line 408
  30. theorem OAI.Erdos970.WeightedTorusJets.Deformation.parameterLocalAlgebra_parameter_regular line 420
  31. theorem OAI.Erdos970.WeightedTorusJets.Deformation.flat_ideal_quotient_of_flat_smul_top line 437
  32. theorem OAI.Erdos970.WeightedTorusJets.Deformation.ideal_ofList_ofFn_eq_span_range line 448
  33. theorem OAI.Erdos970.WeightedTorusJets.Deformation.ideal_ofList_map_finRange_eq_span_range line 456
  34. theorem OAI.Erdos970.WeightedTorusJets.Deformation.flat_span_range_quotient_of_flat_ofFn_smul_top line 462
  35. theorem OAI.Erdos970.WeightedTorusJets.Deformation.flat_polynomialDeformation_localized line 476