Commit 2025-10-22 23:09 3d0794dd
View on Github →chore(RingTheory/AdicValuation,LaurentSeries): switch to WithZero.exp instead of coercions of Multiplicative.ofAdd (#29642)
as requested at
https://github.com/leanprover-community/mathlib4/pull/27339#issuecomment-3285102305