mathlib3

b1d8b897 - chore(algebra/char_p): refactor char_p (#5132)