Commit 2025-12-06 11:00 cbb725e8

View on Github →

feat(Algebra/Polynomial/Basic): Add ofMultiset (#32496) Due to a force push I can't reopen #32005. This adds just the definition as described in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Adding.20Polynomial.2EfromRoots.3F/with/558903708 without any refactor.

Estimated changes