mathlib3

9ca3ce6e - chore(data/opposite): pp_nodot on op and unop (#3413)

chore(data/opposite): pp_nodot on op and unop (#3413) Since it's not possible to write `X.op`, its extremely unhelpful for the pretty printer to output this. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>