Commit 2020-08-09 01:11 17ef529d

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).