Commit 2024-11-09 09:51 8d84a980

View on Github →

feat(RingTheory/LaurentSeries): finishes the proof that LaurentSeries are the X-adic completion of Rational Functions (#18346) We add two sections to the file RingTheory/LaurentSeries:

Dense, proving that the rational functions are dense in the Laurent Series
Comparison, providing the isomorphism between the X-adic completion of rational functions with Laurent Series, and then specializing this to an isomorphism between the unit ball in the former with power series.

Estimated changes

Modified Mathlib/RingTheory/LaurentSeries.lean

added theorem LaurentSeries.LaurentSeries_coe

added theorem LaurentSeries.X_order_mul_powerSeriesPart

added theorem LaurentSeries.coe_X_compare

added theorem LaurentSeries.coe_range_dense

added theorem LaurentSeries.comparePkg_eq_extension

added theorem LaurentSeries.continuous_coe

added theorem LaurentSeries.exists_Polynomial_intValuation_lt

added theorem LaurentSeries.exists_powerSeries_of_memIntegers

added theorem LaurentSeries.exists_ratFunc_val_lt

added theorem LaurentSeries.inducing_coe

added theorem LaurentSeries.mem_integers_of_powerSeries

added theorem LaurentSeries.powerSeries_ext_subring

added theorem LaurentSeries.ratfuncAdicComplRingEquiv_apply

added theorem LaurentSeries.tendsto_valuation

added theorem LaurentSeries.valuation_LaurentSeries_equal_extension

added theorem LaurentSeries.valuation_compare