mathlib3

380d6cae - chore(algebra/direct_sum/module): extract out common `variables` (#10207)

chore(algebra/direct_sum/module): extract out common `variables` (#10207) Slight reorganization to extract out repeatedly-used variable declarations, and update module docstring. No changes to the content.