# mathlib3documentation

linear_algebra.free_module.finite.matrix

# Finite and free modules using matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main results #

• module.free.linear_map : if M and N are finite and free, then M →ₗ[R] N is free.
• module.finite.of_basis : A free module with a basis indexed by a fintype is finite.
• module.finite.linear_map : if M and N are finite and free, then M →ₗ[R] N is finite.
@[protected, instance]
def module.free.linear_map (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [ M] [ M] [ N] [ N] [ M] [ N] :
(M →ₗ[R] N)
@[protected, instance]
def module.finite.linear_map {R : Type u} (M : Type v) (N : Type w) [comm_ring R] [ M] [ M] [ N] [ N] [ M] [ N] :
(M →ₗ[R] N)
@[protected, instance]
def module.finite.add_monoid_hom (M : Type v) (N : Type w) [ M] [ M] [ N] [ N] :
(M →+ N)
@[protected, instance]
def module.free.add_monoid_hom (M : Type v) (N : Type w) [ M] [ M] [ N] [ N] :
(M →+ N)
theorem finite_dimensional.finrank_linear_map (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [ M] [ M] [ M] [ N] [ N] [ N] :

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

theorem matrix.rank_vec_mul_vec {K m n : Type u} [comm_ring K] [fintype n] [decidable_eq n] (w : m K) (v : n K) :