mathlib3

8d352b20 - feat(char_p): generalize zmod.neg_one_ne_one (#2796)