# Commit 2020-08-09 01:11 17ef529d

View on Github →refactor(linear_algebra/affine_space): split up file (#3726)
`linear_algebra/affine_space.lean`

was the 10th largest `.lean`

file
in mathlib. Move it to `linear_algebra/affine_space/basic.lean`

and
split out some pieces into separate files, so reducing its size to
41st largest as well as reducing dependencies for users not needing
all those files.
More pieces could also be split out (for example, splitting out
`homothety`

would eliminate the dependence of
`linear_algebra.affine_space.basic`

on
`linear_algebra.tensor_product`

), but this split seems a reasonable
starting point.
This split is intended to preserve the exact set of definitions
present and their namespaces, just moving some of them to different
files, even if the existing namespaces aren't very consistent
(e.g. some definitions relating to affine combinations are in the
`finset`

namespace, so allowing dot notation to be used for such
combinations, but others are in the `affine_space`

namespace, and
there may not be a consistent rule for the division between the two).