OAI/RingTheory/Multiplicity/CoefficientFieldLocalSection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.CoefficientField.localSection line 37
  2. lemma OAI.Lech.CoefficientField.localSection_rightInverse line 44
  3. lemma OAI.Lech.CoefficientField.localSection_injective line 52
  4. lemma OAI.Lech.Normalization.parameter_eval_finite line 66
  5. lemma OAI.Lech.Normalization.parameter_eval_injective line 71
  6. theorem OAI.Lech.Normalization.exists_finite_powerSeries_normalization line 93
  7. theorem OAI.Lech.Normalization.parameter_powers_multiplicity line 127
  8. lemma OAI.Lech.Normalization.radical_span_powers line 189
  9. theorem OAI.Lech.Normalization.parameter_powers_multiplicity_enn line 202
  10. theorem OAI.Lech.Normalization.parameter_frobenius_multiplicity_enn line 227
  11. theorem OAI.Lech.finite_module_colength_error_pos line 262
  12. theorem OAI.Lech.finite_module_asymptotic_pos line 302
  13. theorem OAI.Lech.PowerSeries.finite_module_two_limits_pos line 332
  14. theorem OAI.Lech.PowerSeries.exists_parameter_multiplicity_pos line 416
  15. theorem OAI.Lech.Normalization.parameter_multiplicity_pos line 447