Theorem Polynomial.toFinsupp_nsmul

Modification history

2025-12-17 09:29
Mathlib/Algebra/Polynomial/Basic.lean
feat: avoid `private irreducible_def` using module system (#32861) …
Modified Polynomial.toFinsupp_nsmulView on Github →
2024-11-15 22:23
Mathlib/Algebra/Polynomial/Basic.lean
refactor(Algebra/Polynomial/Basic): define nsmul/zsmul for Polynomial (#19095) …
Added Polynomial.toFinsupp_nsmulView on Github →