divX vs divByMonic X

Stream: mathlib4

[Bolton Bailey]

Is there a particular reason we have docs#Polynomial.divX and a bunch of lemmas about it rather than just using p /ₘ X instead?

[Bolton Bailey]

I guess it's used somehow in the definition of divByMonic?

[Bolton Bailey]

No doesn't seem like it, I can rearrange Data.Polynomial.Div.lean so that if I comment out the import to the definition of divX the definition of divByMonic compiles.

[Eric Rodriguez]

@Eric Wieser i think you made this

[Eric Wieser]

I think I generalized it, not added it; you're thinking of mathlib3#15905

[Eric Rodriguez]

Ahh, I see. it's a shame git blame is harder now :/

[Eric Wieser]

I promise I'll glue the histories together soon!

[Bolton Bailey]

It feels like it would be better to avoid this definition entirely so that people don't have to deal with multiple APIs. Do people care if I try to remove it? What happens to the mathport process if I remove lemmas that have #align statements near them?

[Ruben Van de Velde]

You should replace them by #noaligns

[Eric Wieser]

Am I right in claiming that docs#MvPolynomial.divMonomial is genuinely useful?

[Eric Wieser]

And it's just the specialization to Polynomial that isn't due to docs#Polynomial.divByMonic existing?

[Eric Wieser]

Oh, docs#Polynomial.divByMonic doesn't work on Semirings

[Damiano Testa]

I suspect that divX plays a useful role in formalizing results. My guess is that the "mathematically interesting" facts will be about divByMonic, but that their proofs will (implicitly or explicitly) rely on many recursive applications of divX.