Commit 2024-05-22 08:00 850fd808

View on Github →

feat(LinearAlgebra/{FiniteDimensional|Dimension/DivisionRing}): relax condition of some results (#12963) ... 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. Changed results: In DivisionRing.lean:

  • Basis.ofRankEqZero[_apply]
  • le_rank_iff_exists_linearIndependent[_finset]
  • rank[_submodule]_le_one_iff, rank_submodule_le_one_iff'
  • newly added result: rank[_submodule]_eq_one_iff
  • Submodule.rank_le_one_iff_isPrincipal, Module.rank_le_one_iff_top_isPrincipal In FiniteDimensional.lean:
  • finrank_eq_one_iff, finrank_eq_one_iff', finrank_le_one_iff
  • Submodule.finrank_le_one_iff_isPrincipal, Module.finrank_le_one_iff_top_isPrincipal
  • cardinal_mk_eq_cardinal_mk_field_pow_rank, cardinal_lt_aleph0_of_finiteDimensional All of them are moved to a separated file.

Estimated changes

deleted def Basis.ofRankEqZero
deleted theorem Basis.ofRankEqZero_apply
deleted theorem rank_le_one_iff
deleted theorem rank_submodule_le_one_iff
added theorem finrank_eq_one_iff'
added theorem finrank_eq_one_iff
added theorem finrank_le_one_iff
added theorem rank_eq_one_iff
added theorem rank_le_one_iff
deleted theorem finrank_eq_one_iff'
deleted theorem finrank_eq_one_iff
deleted theorem finrank_le_one_iff