feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot

[acmepjz]

trafficstars

... from requiring F being a field to F satisfying StrongRankCondition and S being a free F-module. This makes the original statement a special case.

The changed results are: Subalgebra.eq_bot_of_(rank_le|finrank)_one, Subalgebra.[fin]rank_eq_one_iff and Subalgebra.bot_eq_top_iff_[fin]rank_eq_one.

Since the generalized results don't requiring division ring anymore, they are moved to an eariler file LinearAlgebra/Dimension/FreeAndStrongRankCondition.

The proof need to use a new result bijective_algebraMap_of_linearEquiv which is put into Algebra/Algebra/Basic.

---

discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312849.20relax.20condition.20of.20Subalgebra.2Eeq_bot_of_finrank_one

[acmepjz]

Seems that a lot of results in this file can be relaxed by the same way. Maybe I'll investigate them later. It's welcomed if someone could compile a list of them.

[acmepjz]

Since #12963 is merged, is it a good idea to move the results in this PR to that file?

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

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

[mathlib-bors[bot]]

:v: acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[acmepjz]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style