mathlib3
17ef529d - refactor(linear_algebra/affine_space): split up file (#3726)

Commit
5 years ago
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).
Author
Parents
Loading