# Documentation

Mathlib.LinearAlgebra.FreeModule.Rank

# Extra results about Module.rank#

This file contains some extra results not in LinearAlgebra.Dimension.

@[simp]
theorem rank_finsupp (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] (ι : Type w) :
Module.rank R (ι →₀ M) = *
theorem rank_finsupp' (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] (ι : Type v) :
Module.rank R (ι →₀ M) = *
theorem rank_finsupp_self (R : Type u) [Ring R] (ι : Type w) :
Module.rank R (ι →₀ R) =

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

theorem rank_finsupp_self' (R : Type u) [Ring R] {ι : Type u} :
Module.rank R (ι →₀ R) =

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

@[simp]
theorem rank_directSum (R : Type u) [Ring R] {ι : Type v} (M : ιType w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] :
Module.rank R (⨁ (i : ι), M i) = Cardinal.sum fun i => Module.rank R (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) [] [] :
Module.rank R (Matrix m n R) = *

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 : Type v) (n : Type v) [] [] :
Module.rank R (Matrix m n R) =

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

theorem rank_matrix'' (R : Type u) [Ring R] (m : Type u) (n : Type u) [] [] :
Module.rank R (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_tensorProduct (R : Type u) (M : Type v) (N : Type w) [] [] [Module R M] [] [] [Module R N] [] :

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

theorem rank_tensorProduct' (R : Type u) (M : Type v) [] [] [Module R M] [] (N : Type v) [] [Module R 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).