mathlib

b876e76b - feat(algebra/char_p/two): couple more lemmas + 🏌️ (#10467)

feat(algebra/char_p/two): couple more lemmas + 🏌️ (#10467) Co-authored-by: Eric <ericrboidi@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>