duplicate definition

Stream: general

[FR]

Are docs#polynomial.integral_normalization and docs#normalize_scale_roots almost the same?

[Riccardo Brasca]

It seems so!

[Riccardo Brasca]

The only difference is for p=0

[Junyan Xu]

If you try to merge them you may also consider using docs#finsupp.sum instead of finset.sum over the support, which usually avoids splitting cases for whether an element is in the support or not.

[Junyan Xu]

I just found the PR #6183 was opened last year! But somehow it got abandoned even though to dependencies were merged. @Yuyang Zhao Would you revive it or would you mind if I take over?

[Yuyang Zhao]

I've been busy recently, but I'll be back to mathlib these days.