Commit 2024-07-16 22:44 bcd055b2

View on Github →

chore: (RingTheory/HahnSeries) : Move valuation material to new file (#14807) Valuation-theoretic material is moved to a separate file. Also, minor docstrings adjustments.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

deleted def HahnSeries.addVal

deleted theorem HahnSeries.addVal_apply

deleted theorem HahnSeries.addVal_apply_of_ne

deleted theorem HahnSeries.addVal_le_of_coeff_ne_zero

Created Mathlib/RingTheory/HahnSeries/Valuation.lean

added def HahnSeries.addVal

added theorem HahnSeries.addVal_apply

added theorem HahnSeries.addVal_apply_of_ne

added theorem HahnSeries.addVal_le_of_coeff_ne_zero