mathlib documentation

linear_algebra.free_module.finite.basic

Finite and free modules #

We provide some instances for finite and free modules.

Main results #

@[protected, instance]
noncomputable def module.free.choose_basis_index.fintype (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] [module.free R M] [nontrivial R] [module.finite R M] :

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

Equations
@[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] :
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)
@[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] :
@[protected, instance]
@[protected, instance]