Def Polynomial.toFinsuppIsoLinear

Modification history

2026-11-02 08:15

Mathlib/Algebra/Polynomial/Basic.lean

refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` (#41981) …

Modified Polynomial.toFinsuppIsoLinear View on Github →

2024-12-13 12:32

Mathlib/Algebra/Polynomial/Basic.lean

chore: move `Polynomial.basisMonomials` to a separate file (#19933) …

Added Polynomial.toFinsuppIsoLinear View on Github →