PR #5361: feat(analysis/real/polynomial): preparations fo...

Stream: triage

[Random Issue Bot]

Today I chose PR 5361 for discussion!

feat(analysis/real/polynomial): preparations for Liouville
Created by @Jujian Zhang (@jjaassoonn) on 2020-12-14
Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

[Damiano Testa]

I have been making progress on simplifying the arguments and streamlining the proofs. I have been already adding some lemmas to mathlib, precisely with this goal in mind!