# Finite and free modules using matrices #

We provide some instances for finite and free modules involving matrices.

## Main results #

• Module.Free.linearMap : if M and N are finite and free, then M →ₗ[R] N is free.
• Module.Finite.ofBasis : A free module with a basis indexed by a Fintype is finite.
• Module.Finite.linearMap : if M and N are finite and free, then M →ₗ[R] N is finite.
instance Module.Free.linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [] [Module R M] [] [] [] [Module R N] [Module S N] [] [] :
Equations
• =
instance Module.Finite.linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [] [Module R M] [] [] [] [Module R N] [Module S N] [] [] :
Equations
• =
theorem FiniteDimensional.rank_linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [] [Module R M] [] [] [] [Module R N] [Module S N] [] [] :
theorem FiniteDimensional.finrank_linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [] [Module R M] [] [] [] [Module R N] [Module S N] [] [] :

The finrank of M →ₗ[R] N as an S-module is (finrank R M) * (finrank S N).

theorem FiniteDimensional.rank_linearMap_self (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [] [Module R M] [] [] [Module R S] [] :
theorem FiniteDimensional.finrank_linearMap_self (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [] [Module R M] [] [] [Module R S] [] :
@[deprecated FiniteDimensional.finrank_linearMap_self]
theorem FiniteDimensional.finrank_linear_map' (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [] [Module R M] [] [] [Module R S] [] :

Alias of FiniteDimensional.finrank_linearMap_self.

instance Finite.algHom (K : Type u_1) (M : Type u_2) (L : Type v) [] [Ring M] [Algebra K M] [] [] [] [] [Algebra K L] :
Equations
• =
theorem cardinal_mk_algHom_le_rank (K : Type u_1) (M : Type u_2) (L : Type v) [] [Ring M] [Algebra K M] [] [] [] [] [Algebra K L] :
theorem card_algHom_le_finrank (K : Type u_1) (M : Type u_2) (L : Type v) [] [Ring M] [Algebra K M] [] [] [] [] [Algebra K L] :
instance Module.Finite.addMonoidHom (M : Type v) (N : Type w) [] [] [] [] [] :
Equations
• =
instance Module.Free.addMonoidHom (M : Type v) (N : Type w) [] [] [] [] [] :
Equations
• =
theorem Matrix.rank_vecMulVec {K : Type u} {m : Type u} {n : Type u} [] [] [] (w : mK) (v : nK) :
(Matrix.toLin' (Matrix.vecMulVec w v)).rank 1