mathlib3

7f1ba1a3 - feat(algebra/char_p/two): add `simp` attribute to some lemmas involving characteristic two identities (#12800)

feat(algebra/char_p/two): add `simp` attribute to some lemmas involving characteristic two identities (#12800) I hope that these `simp` attributes will make working with `char_p R 2` smooth! I felt clumsy with this section, so hopefully this is an improvement.