mathlib3

1e4da8d5 - refactor(linear_algebra/{tensor,exterior}_algebra): convert to a directory (#11513)

refactor(linear_algebra/{tensor,exterior}_algebra): convert to a directory (#11513) These files can be quite slow, so it's useful to be able to add new definitions and lemmas in standalone files, rather than in the same file. There are a number of open PRs of mine that make this move as part of a new feature, so let's just move them pre-emptively.