mathlib

e41b917c - feat(char_p/quotient): Add a lemma to inherit char_p from the underlying ring (#5809)