Commit 2024-10-03 19:18 0c13e183

View on Github →

chore: Rename FiniteDimensional.finrank to Module.finrank (#17192) The namespacing in the linear algebra/affine spaces part of the library is a bit suboptimal. Here are a few arguments for why FiniteDimensional.finrank should be renamed to Module.finrank:

  1. Other objects in maths can be finite-dimensional and have a rank.
  2. finrank is directly analogous to Module.rank, they have lemmas in common (eg finrank_eq_rank, which is currently in neither of the declarations' namespaces) and have common series of lemmas that relate to other declarations in the Module namespace, eg Module.Finite.
  3. We are in the process of replacing FiniteDimensional by Module.Finite, so the FiniteDimensional namespace will soon be obsolete.
  4. It is a shorter and clearer name. Also make Module.Finite protected to avoid clashes with Finite

Estimated changes

deleted theorem Submodule.map_zero
modified theorem Quaternion.finrank_eq_four
modified theorem card_eq_pow_finrank
modified theorem GaloisField.finrank
modified theorem MvPolynomial.finrank_R
added theorem Module.finrank_fin_fun
added theorem Module.finrank_finsupp
added theorem Module.finrank_matrix
added theorem Module.finrank_pi
added theorem Module.finrank_prod
added theorem Module.finrank_pos
added theorem Module.finrank_pos_iff
deleted theorem Module.rank_lt_alpeh0_iff
added theorem Module.finrank_eq_rank
added theorem Module.finrank_self
added theorem Module.rank_lt_aleph0
added theorem Module.rank_self
deleted theorem finrank_eq_nat_card_basis
deleted theorem finrank_eq_rank
deleted theorem rank_lt_aleph0
deleted theorem rank_self
modified theorem Module.finite_dual_iff
added theorem Module.rank_linearMap
modified theorem FDRep.char_one
modified theorem Module.Finite.equiv
modified theorem Module.Finite.equiv_iff
modified theorem Module.Finite.exists_fin'
modified theorem Module.Finite.exists_fin
modified theorem Module.Finite.of_surjective