feat(RingTheory/Flat/Basic): add `lTensor_preserves_injective_linearMap`

[acmepjz]

also move lTensor_inj_iff_rTensor_inj to LinearMap

---

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[alreadydone]

Sorry, there seems to be a build error in Flat.lean

[acmepjz]

Sorry, there seems to be a build error in Flat.lean

Oops. I'll check now.

[EDIT] That bug is very strange; rw [LinearMap.lTensor_inj_iff_rTensor_inj] or rw [L.lTensor_inj_iff_rTensor_inj M] works, but not rw [L.lTensor_inj_iff_rTensor_inj].

---

Also, I marked an existing theorem as deprecated, so it's expected that there are more errors in downstream files. 😂 Now we need to find out all the occurrences of it and got them replaced.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style