# Documentation

Mathlib.LinearAlgebra.FreeModule.Finite.Rank

# Rank of finite free modules #

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

@[simp]
theorem FiniteDimensional.Submodule.finrank_map_subtype_eq (R : Type u) (M : Type v) [Ring R] [] [Module R M] (p : ) (q : Submodule R { x // x p }) :
@[simp]
theorem FiniteDimensional.finrank_ulift (R : Type u) (M : Type v) [Ring R] [] [Module R M] :
theorem FiniteDimensional.rank_lt_aleph0 (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] :

The rank of a finite module is finite.

@[simp]
theorem FiniteDimensional.finrank_eq_rank (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] :
↑() =

If M is finite, finrank M = rank M.

theorem FiniteDimensional.finrank_eq_card_chooseBasisIndex (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] [] :

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

@[simp]

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

theorem FiniteDimensional.finrank_pi (R : Type u) [Ring R] {ι : Type v} [] :

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

@[simp]
theorem FiniteDimensional.finrank_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)] [∀ (i : ι), Module.Finite R (M i)] :
FiniteDimensional.finrank R (⨁ (i : ι), M i) = Finset.sum Finset.univ fun i =>

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

@[simp]
theorem FiniteDimensional.finrank_prod (R : Type u) (M : Type v) (N : Type w) [Ring R] [] [Module R M] [] [] [] [Module R N] [] [] :

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

theorem FiniteDimensional.finrank_pi_fintype (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)] [∀ (i : ι), Module.Finite R (M i)] :
FiniteDimensional.finrank R ((i : ι) → M i) = Finset.sum Finset.univ fun i =>

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

theorem FiniteDimensional.finrank_matrix (R : Type u) [Ring R] (m : Type u_1) (n : Type u_2) [] [] :

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

theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq {R : Type u} {M : Type v} {N : Type w} [Ring R] [] [Module R M] [] [] [] [Module R N] [] [] (cond : ) :

Two finite and free modules are isomorphic if they have the same (finite) rank.

theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq {R : Type u} {M : Type v} {N : Type w} [Ring R] [] [Module R M] [] [] [] [Module R N] [] [] :

Two finite and free modules are isomorphic if and only if they have the same (finite) rank.

noncomputable def LinearEquiv.ofFinrankEq {R : Type u} (M : Type v) (N : Type w) [Ring R] [] [Module R M] [] [] [] [Module R N] [] [] (cond : ) :

Two finite and free modules are isomorphic if they have the same (finite) rank.

Instances For
@[simp]
theorem FiniteDimensional.finrank_tensorProduct (R : Type u) [] (M : Type v) (N : Type w) [] [Module R M] [] [] [Module R N] [] :

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

theorem LinearMap.finrank_le_finrank_of_injective {R : Type u} {M : Type v} {N : Type w} [Ring R] [] [Module R M] [] [Module R N] [] {f : M →ₗ[R] N} (hf : ) :
theorem LinearMap.finrank_range_le {R : Type u} {M : Type v} {N : Type w} [Ring R] [] [Module R M] [] [Module R N] [] (f : M →ₗ[R] N) :
theorem Submodule.finrank_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (s : ) :

The dimension of a submodule is bounded by the dimension of the ambient space.

theorem Submodule.finrank_quotient_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (s : ) :

The dimension of a quotient is bounded by the dimension of the ambient space.

theorem Submodule.finrank_map_le {R : Type u} {M : Type v} {N : Type w} [Ring R] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) (p : ) [Module.Finite R { x // x p }] :

Pushforwards of finite submodules have a smaller finrank.

theorem Submodule.finrank_le_finrank_of_le {R : Type u} {M : Type v} [Ring R] [] [Module R M] {s : } {t : } [Module.Finite R { x // x t }] (hst : s t) :