Commit 2025-01-27 10:06 2bce15bb

View on Github →

feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) Define an Algebra K RatFuncAdicCompl K instance on RatFuncAdicCompl K and promote the already defined ring equivalences to algebra equivalences LaurentSeriesAlgEquiv : K⸨X⸩ ≃ₐ[K] RatFuncAdicCompl K and K⟦X⟧ ≃ₐ[K] (idealX K).adicCompletionIntegers (RatFunc K). TODO : update docstring (on top of file)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

added def LaurentSeries.LaurentSeriesAlgEquiv

added theorem LaurentSeries.LaurentSeriesRingEquiv_def

added theorem LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring

added theorem LaurentSeries.algebraMap_C_mem_adicCompletionIntegers

added theorem LaurentSeries.algebraMap_apply

added def LaurentSeries.powerSeriesAlgEquiv

added theorem LaurentSeries.powerSeriesEquivSubring_apply

added theorem LaurentSeries.powerSeriesEquivSubring_coe_apply

added theorem LaurentSeries.powerSeriesRingEquiv_coe_apply