mathlib3

edfb391a - chore(algebra/module/basic): reduce imports (#17042)

chore(algebra/module/basic): reduce imports (#17042) Avoids importing `algebra.big_operators.basic` in a few files that don't need it. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>