mathlib3

1db04677 - feat(data/polynomial): `adjoin_root.mk_ne_zero` lemmas (#18113)

feat(data/polynomial): `adjoin_root.mk_ne_zero` lemmas (#18113) + `mk_ne_zero_of_(nat_)degree_lt`: if `f : R[X]` is monic and `g : R[X]` is nonzero with (nat_)degree less than (nat_)degree of `f`, then the image of `g` in `R[X]/(f)` is nonzero. Depends on new lemmas `monic.not_dvd_of_(nat_)degree_lt`. + Use it to golf `weierstrass_curve.X/Y_class_ne_zero`. + Move misplaced lemma `nat_degree_lt_nat_degree`.