Rank of finite free modules #
This is a basic API for the rank of finite free modules.
theorem
module.free.rank_lt_aleph_0
(R : Type u)
(M : Type v)
[ring R]
[strong_rank_condition R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M] :
The rank of a finite and free module is finite.
@[simp]
theorem
module.free.finrank_eq_rank
(R : Type u)
(M : Type v)
[ring R]
[strong_rank_condition R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M] :
↑(finite_dimensional.finrank R M) = module.rank R M
theorem
module.free.finrank_eq_card_choose_basis_index
(R : Type u)
(M : Type v)
[ring R]
[strong_rank_condition R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R 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 ι] :
finite_dimensional.finrank R (ι →₀ R) = fintype.card ι
The finrank of (ι →₀ R) is fintype.card ι.
theorem
module.free.finrank_pi
(R : Type u)
[ring R]
[strong_rank_condition R]
{ι : Type v}
[fintype ι] :
finite_dimensional.finrank R (ι → R) = fintype.card ι
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]
theorem
module.free.finrank_prod
(R : Type u)
(M : Type v)
(N : Type w)
[ring R]
[strong_rank_condition R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
[add_comm_group N]
[module R N]
[module.free R N]
[module.finite R N] :
finite_dimensional.finrank R (M × N) = finite_dimensional.finrank R M + finite_dimensional.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.
theorem
module.free.finrank_matrix
(R : Type u)
[ring R]
[strong_rank_condition R]
(m n : Type v)
[fintype m]
[fintype n] :
finite_dimensional.finrank R (matrix m n R) = fintype.card m * fintype.card n
If m and n are fintype, the finrank of m × n matrices is
(fintype.card m) * (fintype.card n).
@[simp]
theorem
module.free.finrank_tensor_product
(R : Type u)
[comm_ring R]
[strong_rank_condition R]
(M : Type v)
(N : Type w)
[add_comm_group M]
[module R M]
[module.free R M]
[add_comm_group N]
[module R N]
[module.free R N] :