mathlib3

b3ce8837 - feat(algebra/*_power): simplify `(-a)^(bit0 _)` and `(-a)^(bit1 _)` (#4573)