Commit 2024-01-01 14:48 0b41ea95

View on Github →

chore: Reorganize results about rank and finrank. (#9349) The files Mathlib.LinearAlgebra.FreeModule.Rank, Mathlib.LinearAlgebra.FreeModule.Finite.Rank, Mathlib.LinearAlgebra.Dimension and Mathlib.LinearAlgebra.Finrank were reorganized into a folder Mathlib.LinearAlgebra.Dimension, containing the following files

  • Basic.lean: Contains the definition of Module.rank.
  • Finrank.lean: Contains the definition of FiniteDimensional.finrank.
  • StrongRankCondition.lean: Contains results about rank and finrank over rings satisfying strong rank condition
  • Free.lean: Contains results about rank and finrank of free modules
  • Finite.lean: Contains conditions or consequences for rank to be finite or zero
  • Constructions.lean: Contains the calculation of the rank of various constructions.
  • DivisionRing.lean: Contains results about rank and finrank of spaces over division rings.
  • LinearMap.lean: Contains results about LinearMap.rank API changes: IsNoetherian.rank_lt_aleph0 and FiniteDimensional.rank_lt_aleph0 are replaced with rank_lt_aleph0. Module.Free.finite_basis was renamed to Module.Finite.finite_basis. FiniteDimensional.finrank_eq_rank was renamed to finrank_eq_rank. rank_eq_cardinal_basis and rank_eq_cardinal_basis' were removed in favour of Basis.mk_eq_mk and Basis.mk_eq_mk''.

Estimated changes

deleted theorem Basis.card_le_card_of_le
deleted def Basis.indexEquiv
deleted theorem Basis.le_span''
deleted theorem Basis.le_span
deleted theorem Basis.mk_eq_rank''
deleted theorem Basis.mk_eq_rank'.{m}
deleted theorem Basis.mk_eq_rank
deleted theorem Basis.mk_range_eq_rank
deleted def Basis.ofRankEqZero
deleted theorem Basis.ofRankEqZero_apply
deleted theorem Ideal.rank_eq
deleted theorem LinearEquiv.lift_rank_eq
deleted theorem LinearEquiv.rank_eq
deleted theorem LinearEquiv.rank_map_eq
deleted theorem LinearMap.rank_add_le
deleted theorem LinearMap.rank_comp_le
deleted theorem LinearMap.rank_le_domain
deleted theorem LinearMap.rank_le_range
deleted theorem LinearMap.rank_zero
deleted theorem basis_le_span'
deleted theorem lift_rank_map_le
deleted theorem lift_rank_range_le
deleted theorem linearIndependent_le_span
deleted theorem mk_eq_mk_of_basis'
deleted theorem mk_eq_mk_of_basis
deleted theorem rank_add_rank_split
deleted theorem rank_bot
deleted theorem rank_eq_card_basis
deleted theorem rank_eq_of_equiv_equiv
deleted theorem rank_eq_of_surjective
deleted theorem rank_eq_zero_iff
deleted theorem rank_fin_fun
deleted theorem rank_fun'
deleted theorem rank_fun
deleted theorem rank_fun_eq_lift_mul
deleted theorem rank_le
deleted theorem rank_le_card
deleted theorem rank_le_of_submodule
deleted theorem rank_le_one_iff
deleted theorem rank_map_le
deleted theorem rank_pi
deleted theorem rank_pos
deleted theorem rank_pos_iff_nontrivial
deleted theorem rank_prod'
deleted theorem rank_prod
deleted theorem rank_punit
deleted theorem rank_quotient_add_rank
deleted theorem rank_quotient_add_rank_le
deleted theorem rank_quotient_le
deleted theorem rank_range_add_rank_ker
deleted theorem rank_range_le
deleted theorem rank_range_of_injective
deleted theorem rank_range_of_surjective
deleted theorem rank_self
deleted theorem rank_span
deleted theorem rank_span_finset_le
deleted theorem rank_span_le
deleted theorem rank_span_le_of_finite
deleted theorem rank_span_of_finset
deleted theorem rank_span_set
deleted theorem rank_submodule_le
deleted theorem rank_submodule_le_one_iff
deleted theorem rank_subsingleton
deleted theorem rank_top
deleted theorem rank_ulift
deleted theorem rank_zero_iff
deleted theorem rank_zero_iff_forall_zero
added theorem LinearEquiv.rank_eq
added theorem lift_rank_map_le
added theorem lift_rank_range_le
added theorem rank_eq_of_equiv_equiv
added theorem rank_le_card
added theorem rank_le_of_submodule
added theorem rank_map_le
added theorem rank_range_le
added theorem rank_submodule_le
added theorem rank_subsingleton
added theorem rank_top
added theorem Subalgebra.finrank_bot
added theorem Subalgebra.rank_bot
added theorem Subalgebra.rank_top
added theorem Submodule.finrank_le
added theorem finrank_ulift
added theorem rank_directSum
added theorem rank_fin_fun
added theorem rank_finsupp'
added theorem rank_finsupp
added theorem rank_finsupp_self'
added theorem rank_finsupp_self
added theorem rank_fun'
added theorem rank_fun
added theorem rank_fun_eq_lift_mul
added theorem rank_matrix''
added theorem rank_matrix'
added theorem rank_matrix
added theorem rank_pi
added theorem rank_prod'
added theorem rank_prod
added theorem rank_quotient_le
added theorem rank_span_finset_le
added theorem rank_span_le_of_finite
added theorem rank_span_of_finset
added theorem rank_tensorProduct'
added theorem rank_tensorProduct
added theorem rank_ulift
added theorem finrank_range_le_card
added theorem finrank_span_eq_card
added theorem finrank_span_le_card
added theorem lift_rank_lt_rank_dual
added theorem rank_add_rank_split
added theorem rank_eq_of_surjective
added theorem rank_fun_infinite
added theorem rank_le_one_iff
added theorem rank_lt_rank_dual'
added theorem rank_lt_rank_dual
added theorem rank_quotient_add_rank
added theorem rank_span_le
added theorem Submodule.rank_eq_zero
added theorem finrank_bot
added theorem finrank_eq_one
added theorem finrank_le_one
added theorem rank_bot
added theorem rank_eq_one
added theorem rank_eq_zero_iff
added theorem rank_le
added theorem rank_pos
added theorem rank_punit
added theorem rank_subsingleton'
added theorem rank_zero_iff
added theorem LinearEquiv.finrank_eq
added theorem finrank_top
added theorem LinearMap.rank_add_le
added theorem LinearMap.rank_comp_le
added theorem LinearMap.rank_zero
added def Basis.indexEquiv
added theorem Basis.le_span''
added theorem Basis.le_span
added theorem Basis.mk_eq_rank''
added theorem Basis.mk_eq_rank'.{m}
added theorem Basis.mk_eq_rank
added theorem Basis.mk_range_eq_rank
added theorem Ideal.rank_eq
added theorem basis_le_span'
added theorem finrank_eq_rank
added theorem mk_eq_mk_of_basis'
added theorem mk_eq_mk_of_basis
added theorem rank_eq_card_basis
added theorem rank_lt_aleph0
added theorem rank_self
added theorem rank_span
added theorem rank_span_set
deleted theorem LinearEquiv.finrank_eq
deleted theorem Subalgebra.finrank_bot
deleted theorem Subalgebra.rank_bot
deleted theorem Subalgebra.rank_top
deleted theorem finrank_bot
deleted theorem finrank_eq_nat_card_basis
deleted theorem finrank_eq_one
deleted theorem finrank_le_one
deleted theorem finrank_range_le_card
deleted theorem finrank_span_eq_card
deleted theorem finrank_span_le_card
deleted theorem finrank_span_set_eq_card
deleted theorem finrank_top
deleted theorem Module.Free.finite_basis
deleted theorem LinearIndependent.finite
deleted theorem Module.rank_lt_alpeh0_iff
deleted theorem Submodule.finrank_eq_zero
deleted theorem Submodule.finrank_le
deleted theorem Submodule.finrank_map_le
deleted theorem Submodule.rank_eq_zero
deleted theorem lift_rank_lt_rank_dual'
deleted theorem lift_rank_lt_rank_dual
deleted theorem rank_directSum
deleted theorem rank_eq_cardinal_basis'
deleted theorem rank_eq_cardinal_basis
deleted theorem rank_finsupp'
deleted theorem rank_finsupp
deleted theorem rank_finsupp_self'
deleted theorem rank_finsupp_self
deleted theorem rank_fun_infinite
deleted theorem rank_lt_rank_dual'
deleted theorem rank_lt_rank_dual
deleted theorem rank_matrix''
deleted theorem rank_matrix'
deleted theorem rank_matrix
deleted theorem rank_tensorProduct'
deleted theorem rank_tensorProduct