mathlib

c4a34136 - chore(data/polynomial): use dot notation for monic lemmas (#12530)

chore(data/polynomial): use dot notation for monic lemmas (#12530) As discussed in #12447 - Use the notation throughout the library - Also deleted `ne_zero_of_monic` as it was a duplicate of `monic.ne_zero` it seems. - Cleaned up a small proof here and there too. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Eric <ericrboidi@gmail.com>