Def Polynomial.erase

Modification history

2026-11-02 08:15

Mathlib/Algebra/Polynomial/Basic.lean

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

Deleted Polynomial.erase View on Github →

2026-10-28 01:05

Mathlib/Algebra/Polynomial/Basic.lean

chore: replace `irreducible_def` with `no_expose` (#45063) …

Added Polynomial.erase View on Github →