Commit 2022-08-10 15:00 473da0e0

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!