# Rank of free modules #

## Main result #

• LinearEquiv.nonempty_equiv_iff_lift_rank_eq: Two free modules are isomorphic iff they have the same dimension.
• FiniteDimensional.finBasis: An arbitrary basis of a finite free module indexed by Fin n given finrank R M = n.
theorem lift_rank_mul_lift_rank (F : Type u) (K : Type v) (A : Type w) [Ring F] [Ring K] [] [Module F K] [Module K A] [Module F A] [] [] [] :
* =

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

The universe polymorphic version of rank_mul_rank below.

theorem rank_mul_rank (F : Type u) (K : Type v) [Ring F] [Ring K] [Module F K] [] (A : Type v) [] [Module K A] [Module F A] [] [] :
* =

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

This is a simpler version of lift_rank_mul_lift_rank with K and A in the same universe.

theorem FiniteDimensional.finrank_mul_finrank (F : Type u) (K : Type v) (A : Type w) [Ring F] [Ring K] [] [Module F K] [Module K A] [Module F A] [] [] [] :

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

theorem Module.Free.rank_eq_card_chooseBasisIndex (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] :

The rank of a free module M over R is the cardinality of ChooseBasisIndex R 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.

theorem Module.Free.rank_eq_mk_of_infinite_lt (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] [] (h_lt : < ) :
=

The rank of a free module M over an infinite scalar ring R is the cardinality of M whenever #R < #M.

theorem nonempty_linearEquiv_of_lift_rank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [] [Module R M] [] [] [Module R M'] [Module.Free R M'] (cnd : = ) :

Two vector spaces are isomorphic if they have the same dimension.

theorem nonempty_linearEquiv_of_rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [] [Module R M] [] [] [Module R M₁] [Module.Free R M₁] (cond : = Module.rank R M₁) :
Nonempty (M ≃ₗ[R] M₁)

Two vector spaces are isomorphic if they have the same dimension.

def LinearEquiv.ofLiftRankEq {R : Type u} (M : Type v) (M' : Type v') [Ring R] [] [Module R M] [] [] [Module R M'] [Module.Free R M'] (cond : = ) :
M ≃ₗ[R] M'

Two vector spaces are isomorphic if they have the same dimension.

Equations
Instances For
def LinearEquiv.ofRankEq {R : Type u} (M : Type v) (M₁ : Type v) [Ring R] [] [Module R M] [] [] [Module R M₁] [Module.Free R M₁] (cond : = Module.rank R M₁) :
M ≃ₗ[R] M₁

Two vector spaces are isomorphic if they have the same dimension.

Equations
Instances For
theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [] [Module R M] [] [] [Module R M'] [Module.Free R M'] :

Two vector spaces are isomorphic if and only if they have the same dimension.

theorem LinearEquiv.nonempty_equiv_iff_rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [] [Module R M] [] [] [Module R M₁] [Module.Free R M₁] :
Nonempty (M ≃ₗ[R] M₁) = Module.rank R M₁

Two vector spaces are isomorphic if and only if they have the same dimension.

theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [] [Module R M] [] [] [Module R M'] [Module.Free R M'] [] [] (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} {M' : Type v'} [Ring R] [] [Module R M] [] [] [Module R M'] [Module.Free R M'] [] [] :

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) (M' : Type v') [Ring R] [] [Module R M] [] [] [Module R M'] [Module.Free R M'] [] [] (cond : ) :
M ≃ₗ[R] M'

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

Equations
Instances For
theorem Module.rank_lt_alpeh0_iff {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] :

See rank_lt_aleph0 for the inverse direction without Module.Free R M.

theorem FiniteDimensional.finrank_of_not_finite {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (h : ¬) :
theorem Module.finite_of_finrank_pos {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (h : ) :
theorem Module.finite_of_finrank_eq_succ {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] {n : } (hn : = n.succ) :
theorem Module.finite_iff_of_rank_eq_nsmul {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] {W : Type v} [] [Module R W] [] {n : } (hn : n 0) (hVW : = n ) :
noncomputable def FiniteDimensional.finBasis (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] [] :
Basis (Fin ) R M

A finite rank free module has a basis indexed by Fin (finrank R M).

Equations
• = .reindex
Instances For
noncomputable def FiniteDimensional.finBasisOfFinrankEq (R : Type u) (M : Type v) [Ring R] [] [Module R M] [] [] {n : } (hn : ) :
Basis (Fin n) R M

A rank n free module has a basis indexed by Fin n.

Equations
Instances For
noncomputable def FiniteDimensional.basisUnique {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] (ι : Type u_1) [] (h : ) :
Basis ι R M

A free module with rank 1 has a basis with one element.

Equations
Instances For
@[simp]
theorem FiniteDimensional.basisUnique_repr_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] {ι : Type u_1} [] {h : } {v : M} {i : ι} :
(.repr v) i = 0 v = 0