Commit 2026-09-02 12:58 b38bb28c

View on Github →

refactor(Algebra/Polynomial): make coeff return a Finsupp (#41544) This matches AddMonoidAlgebra. Change made by myself, build fixed by Claude Opus, with the fixes reviewed by myself again. Assisted-by: Claude Opus 4.8

Estimated changes

Modified Counterexamples/MapFloor.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

modified def Polynomial.coeff

modified theorem Polynomial.coeff_injective

Modified Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean

Modified Mathlib/Data/Nat/Choose/Lucas.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

Modified Mathlib/RingTheory/Polynomial/Vieta.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/Tactic/ComputeDegree.lean