Commit 2025-08-11 10:26 e704c683

View on Github →

feat(RingTheory): add HahnSeries.ofFinsupp (#28136) Part of #27043 Hahn's embedding theorem

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.coeff_ofFinsuppLinearMap

added def HahnSeries.ofFinsuppLinearMap

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.coeff_ofFinsupp

added def HahnSeries.ofFinsupp