Commit 2024-05-24 11:39 28d9a940

feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot (#12849) ... 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.