[Merged by Bors] - chore: remove LinearAlgebra.Basic

[Ruben-VandeVelde]

It had become an incoherent grab-bag of results, which I've moved to more suitable places over the last few months.

---

• depends on: [Merged by Bors] - chore: redistribute a few results from Algebra.Module.Submodule.LinearMap #12295
• depends on: [Merged by Bors] - chore: remove redundant LinearEquiv.map_neg/sub #12330
• depends on: [Merged by Bors] - chore: move LinearMap.range into its own file #12378
• depends on: [Merged by Bors] - chore: move the link between additive morphisms and linear maps earlier #12457
• depends on: [Merged by Bors] - chore: move LinearMap.eqLocus to its own file #13566
• depends on: [Merged by Bors] - chore: move basic linear equivalences to Mathlib.Algebra.Module.Equiv #13662
• depends on: [Merged by Bors] - chore: move linear equivalences about submodules to Algebra.Module.Submodule.Equiv #13684
• depends on: [Merged by Bors] - chore: move IsLinearMap theorems to their own file #14116

[github-actions]

PR summary 719068078a

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Basic	639	0	-639 (-100.00%)

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: redistribute a few results from Algebra.Module.Submodule.LinearMap #12295
• [Merged by Bors] - chore: remove redundant LinearEquiv.map_neg/sub #12330
• [Merged by Bors] - chore: move LinearMap.range into its own file #12378
• [Merged by Bors] - chore: move the link between additive morphisms and linear maps earlier #12457
• [Merged by Bors] - chore: move LinearMap.eqLocus to its own file #13566
• [Merged by Bors] - chore: move basic linear equivalences to Mathlib.Algebra.Module.Equiv #13662
• [Merged by Bors] - chore: move linear equivalences about submodules to Algebra.Module.Submodule.Equiv #13684
• [Merged by Bors] - chore: move IsLinearMap theorems to their own file #14116
  By Dependent Issues (🤖). Happy coding!

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style