mathlib3 documentation

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 #

@[protected, instance]
def module.free.linear_map (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] [module.finite R M] [module.finite R N] :
@[protected, instance]
def module.finite.linear_map {R : Type u} (M : Type v) (N : Type w) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] [module.finite R M] [module.finite R N] :

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