mathlib3

6796beeb - chore(algebra/char_p/basic): generalize to non_assoc_semiring (#7985)