OAI/RingTheory/Multiplicity/PowerSeriesFinDimension.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.PowerSeries.fin_dimension_nat line 33
  2. theorem OAI.Lech.PowerSeries.finite_module_two_limits line 38
  3. lemma OAI.Lech.LocalAlgebra.quotient_length_eq line 117
  4. theorem OAI.Lech.PowerSeries.parameter_powers_limit line 140
  5. def OAI.Lech.PowerSeries.eval line 175
  6. lemma OAI.Lech.PowerSeries.eval_C line 186
  7. lemma OAI.Lech.PowerSeries.eval_X line 199
  8. def OAI.Lech.PowerSeries.variablesIdeal line 219
  9. lemma OAI.Lech.PowerSeries.polynomial_variables_map line 222
  10. lemma OAI.Lech.PowerSeries.completion_variables_map line 229
  11. lemma OAI.Lech.PowerSeries.complete_variables line 240
  12. lemma OAI.Lech.AdicNakayama.lift_power line 250
  13. theorem OAI.Lech.AdicNakayama.surjective line 264
  14. lemma OAI.Lech.AdicNakayama.mem_smul_top_pi line 283
  15. lemma OAI.Lech.AdicNakayama.precomplete_pi line 297
  16. theorem OAI.Lech.AdicNakayama.finite_of_quotient line 315
  17. lemma OAI.Lech.Normalization.finite_primary_quotient line 334
  18. theorem OAI.Lech.Normalization.finite_parameter_algebra line 367
  19. lemma OAI.Lech.Normalization.exists_parameters line 410
  20. def OAI.Lech.CoefficientField.frobeniusFactor line 444
  21. lemma OAI.Lech.CoefficientField.frobeniusFactor_mk line 452
  22. def OAI.Lech.CoefficientField.stage line 457
  23. lemma OAI.Lech.CoefficientField.stage_pow_mk line 460
  24. lemma OAI.Lech.CoefficientField.power_strictMono line 469
  25. lemma OAI.Lech.CoefficientField.stage_compatible line 472
  26. def OAI.Lech.CoefficientField.sectionMap line 495
  27. lemma OAI.Lech.CoefficientField.sectionMap_mod line 499
  28. theorem OAI.Lech.CoefficientField.sectionMap_rightInverse line 504
  29. lemma OAI.Lech.CoefficientField.sectionMap_injective line 513