mathlib

aff951a5 - chore(algebra/big_operators): don't use omega (#3255)

chore(algebra/big_operators): don't use omega (#3255) Postpone importing `omega` a little bit longer. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>