mathlib documentation


Finite and free modules #

We provide some instances for finite and free modules.

Main results #

@[protected, instance]

If a free module is finite, then any basis is finite.

theorem module.finite.of_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] [finite ι] (b : basis ι R M) :

A free module with a basis indexed by a fintype is finite.

@[protected, instance]
def module.finite.matrix {R : Type u} [comm_ring R] {ι₁ : Type u_1} {ι₂ : Type u_2} [finite ι₁] [finite ι₂] :
module.finite R (matrix ι₁ ι₂ R)