mathlib3

473da0e0 - feat(data/polynomial/{ basic + div + monic + degree/definitions }): lemmas about monic and forall_eq (#15817)

feat(data/polynomial/{ basic + div + monic + degree/definitions }): lemmas about monic and forall_eq (#15817) This PR reorganizes a couple of lemmas about monic. The main breaking change is the removal of `subsingleton_of_monic_zero'` in favour of `monic_zero_iff_subsingleton`. I left in `monic_zero_iff_subsingleton'` an iff version of `subsingleton_of_monic_zero'`, but I think that this can probably be removed, thanks to `monic_zero_iff_subsingleton` and `forall_eq_iff_forall_eq`. Also, if anyone wants to rename some/all subsingletons to forall_eq, I am happy to do the change!