Commit 2024-07-20 15:43 9654ac4d

View on Github →

chore: speed up by changing def to abbrev in RingTheory/PowerSeries/Basic (#14913) Fixes a 7-10s build delay in RingTheory/PowerSeries/Basic, due to convert idling, by changing def to abbrev. Which uncovered a diamond (unwanted RatFunc.instCoePolynomial). https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/compiling.20behaviour.20within.20one.20file

Estimated changes

Modified Mathlib/RingTheory/LaurentSeries.lean

modified theorem RatFunc.coe_coe

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

deleted def PowerSeries

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean