# mathlib3documentation

linear_algebra.free_module.rank

# Extra results about module.rank#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains some extra results not in linear_algebra.dimension.

@[simp]
theorem rank_finsupp (R : Type u) (M : Type v) [ring R] [ M] [ M] (ι : Type w) :
→₀ M) = (cardinal.mk ι).lift * M).lift
theorem rank_finsupp' (R : Type u) (M : Type v) [ring R] [ M] [ M] (ι : Type v) :
→₀ M) = * M
@[simp]
theorem rank_finsupp_self (R : Type u) [ring R] (ι : Type w) :
→₀ R) = (cardinal.mk ι).lift

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

theorem rank_finsupp_self' (R : Type u) [ring R] {ι : Type u} :
→₀ R) =

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

@[simp]
theorem 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 rank_matrix (R : Type u) [ring R] (m : Type v) (n : Type w) [finite m] [finite n] :

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

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

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

@[simp]
theorem rank_matrix'' (R : Type u) [ring R] (m n : Type u) [finite m] [finite n] :
(matrix m n R) =

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

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

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

theorem 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).