mathlib documentation

linear_algebra.free_module.finite.rank

Rank of finite free modules #

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

The rank of a finite and free module is finite.

@[simp]

If M is finite and free, finrank M = rank M.

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

@[simp]
theorem module.free.finrank_finsupp (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} [fintype ι] :

The finrank of (ι →₀ R) is fintype.card ι.

theorem module.free.finrank_pi (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} [fintype ι] :

The finrank of (ι → R) is fintype.card ι.

@[simp]
theorem module.free.finrank_direct_sum (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} [fintype ι] (M : ι → Type w) [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [∀ (i : ι), module.free R (M i)] [∀ (i : ι), module.finite R (M i)] :
finite_dimensional.finrank R (direct_sum ι (λ (i : ι), M i)) = finset.univ.sum (λ (i : ι), finite_dimensional.finrank R (M i))

The finrank of the direct sum is the sum of the finranks.

@[simp]

The finrank of M × N is (finrank R M) + (finrank R N).

theorem module.free.finrank_pi_fintype (R : Type u) [ring R] [strong_rank_condition R] {ι : Type v} [fintype ι] {M : ι → Type w} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [∀ (i : ι), module.free R (M i)] [∀ (i : ι), module.finite R (M i)] :
finite_dimensional.finrank R (Π (i : ι), M i) = finset.univ.sum (λ (i : ι), finite_dimensional.finrank R (M i))

The finrank of a finite product is the sum of the finranks.

If m and n are fintype, the finrank of m × n matrices is (fintype.card m) * (fintype.card n).

The finrank of M →ₗ[R] N is (finrank R M) * (finrank R N).

@[simp]

The finrank of M ⊗[R] N is (finrank R M) * (finrank R N).