mathlib

2babfeb0 - chore(data/complex/is_R_or_C): squeeze simps (#11251)

chore(data/complex/is_R_or_C): squeeze simps (#11251) This PR squeezes most of the simps in `is_R_or_C`, and updates the module docstring. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>