Commit 2024-10-01 18:15 90a6b826

View on Github →

feat(RingTheory/LaurentSeries): prove that Laurent Series over a field are complete (#16865) In this PR we provide a proof that the Laurent series over a field are complete.

Estimated changes

Modified Mathlib/Order/Filter/Ultrafilter.lean

added theorem Ultrafilter.eq_of_le_pure

Modified Mathlib/RingTheory/LaurentSeries.lean

added def LaurentSeries.Cauchy.coeff

added theorem LaurentSeries.Cauchy.coeff_eventually_equal

added theorem LaurentSeries.Cauchy.coeff_support_bddBelow

added theorem LaurentSeries.Cauchy.coeff_tendsto

added theorem LaurentSeries.Cauchy.eventually_mem_nhds

added theorem LaurentSeries.Cauchy.exists_lb_coeff_ne

added theorem LaurentSeries.Cauchy.exists_lb_eventual_support

added theorem LaurentSeries.Cauchy.exists_lb_support

added def LaurentSeries.Cauchy.limit

added theorem LaurentSeries.uniformContinuous_coeff

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem eq_singleton_left_of_prod_subset_idRel

added theorem eq_singleton_prod_subset_idRel

added theorem eq_singleton_right_prod_subset_idRel

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem UniformSpace.DiscreteUnif.cauchy_le_pure

added theorem UniformSpace.DiscreteUnif.eq_const_of_cauchy