# mathlibdocumentation

linear_algebra.free_module.rank

# Rank of free modules #

This is a basic API for the rank of free modules.

theorem module.free.rank_eq_card_choose_basis_index (R : Type u) (M : Type v) [ring R] [ M] [ M] :
M =

The rank of a free module M over R is the cardinality of choose_basis_index R M.

@[simp]
theorem module.free.rank_finsupp (R : Type u) [ring R] {ι : Type v} :
→₀ R) = (# ι).lift

The rank of (ι →₀ R) is (# ι).lift.

theorem module.free.rank_finsupp' (R : Type u) [ring R] {ι : Type u} :
→₀ R) = # ι

If R and ι lie in the same universe, the rank of (ι →₀ R) is # ι.

@[simp]
theorem module.free.rank_prod (R : Type u) (M : Type v) (N : Type w) [ring R] [ M] [ M] [ N] [ N] :
(M × N) = M).lift + N).lift

The rank of M × N is (module.rank R M).lift + (module.rank R N).lift.

theorem module.free.rank_prod' (R : Type u) (M : Type v) [ring R] [ M] [ M] (N : Type v) [ N] [ N] :
(M × N) = M + N

If M and N lie in the same universe, the rank of M × N is (module.rank R M) + (module.rank R N).

@[simp]
theorem module.free.rank_direct_sum (R : Type u) [ring R] {ι : Type v} (M : ι → Type w) [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] [∀ (i : ι), (M i)] :
(⨁ (i : ι), M i) = cardinal.sum (λ (i : ι), (M i))

The rank of the direct sum is the sum of the ranks.

@[simp]
theorem module.free.rank_pi_fintype (R : Type u) [ring R] {ι : Type v} [fintype ι] {M : ι → Type w} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] [∀ (i : ι), (M i)] :
(Π (i : ι), M i) = cardinal.sum (λ (i : ι), (M i))

The rank of a finite product is the sum of the ranks.

@[simp]
theorem module.free.rank_matrix (R : Type u) [ring R] (n : Type v) [fintype n] (m : Type w) [fintype m] :
(matrix n m R) = ((# n).lift) * (# m).lift

If n and m are fintype, the rank of n × m matrices is (# n).lift * (# m).lift.

@[simp]
theorem module.free.rank_matrix' (R : Type u) [ring R] (n : Type v) [fintype n] (m : Type v) [fintype m] :
(matrix n m R) = ((# n) * # m).lift

If n and m are fintype that lie in the same universe, the rank of n × m matrices is (# n * # m).lift.

@[simp]
theorem module.free.rank_matrix'' (R : Type u) [ring R] (n : Type u) [fintype n] (m : Type u) [fintype m] :
(matrix n m R) = (# n) * # m

If n and m are fintype that lie in the same universe as R, the rank of n × m matrices is # n * # m.

@[simp]
theorem module.free.rank_tensor_product (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [ M] [ M] [ N] [ N] :
(M N) = ((module.rank R M).lift) * N).lift

The rank of M ⊗[R] N is (module.rank R M).lift * (module.rank R N).lift.

theorem module.free.rank_tensor_product' (R : Type u) (M : Type v) [comm_ring R] [ M] [ M] (N : Type v) [ N] [ N] :
(M N) = M) * N

If M and N lie in the same universe, the rank of M ⊗[R] N is (module.rank R M) * (module.rank R N).